Theorem kmlem11 3590

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.

Hypothesis

Ref	Expression
kmlem8.1	⊢ A = {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))}

Assertion

Ref	Expression
kmlem11	⊢ (∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → (∀z ∈ A (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) → ∀z ∈ x (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A)))))

Distinct variable group(s):   x,y,z,v,u,t   y,A,z,v

Proof of Theorem kmlem11

Step	Hyp	Ref	Expression
1		difeq1 1582	. . . . . . . . 9 ⊢ (t = z → (t ∖ ∪(x ∖ {t})) = (z ∖ ∪(x ∖ {t})))
2		sneq 1816	. . . . . . . . . . . 12 ⊢ (t = z → {t} = {z})
3	2	difeq2d 1588	. . . . . . . . . . 11 ⊢ (t = z → (x ∖ {t}) = (x ∖ {z}))
4	3	unieqd 1929	. . . . . . . . . 10 ⊢ (t = z → ∪(x ∖ {t}) = ∪(x ∖ {z}))
5	4	difeq2d 1588	. . . . . . . . 9 ⊢ (t = z → (z ∖ ∪(x ∖ {t})) = (z ∖ ∪(x ∖ {z})))
6	1, 5	eqtrd 1128	. . . . . . . 8 ⊢ (t = z → (t ∖ ∪(x ∖ {t})) = (z ∖ ∪(x ∖ {z})))
7	6	cleq1d 1109	. . . . . . 7 ⊢ (t = z → ((t ∖ ∪(x ∖ {t})) = ∅ ↔ (z ∖ ∪(x ∖ {z})) = ∅))
8	7	negbid 463	. . . . . 6 ⊢ (t = z → (¬ (t ∖ ∪(x ∖ {t})) = ∅ ↔ ¬ (z ∖ ∪(x ∖ {z})) = ∅))
9	8	cbvralv 1333	. . . . 5 ⊢ (∀t ∈ x ¬ (t ∖ ∪(x ∖ {t})) = ∅ ↔ ∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅)
10	6	ineq1d 1644	. . . . . . . 8 ⊢ (t = z → ((t ∖ ∪(x ∖ {t})) ∩ y) = ((z ∖ ∪(x ∖ {z})) ∩ y))
11	10	eleq2d 1156	. . . . . . 7 ⊢ (t = z → (v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y) ↔ v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y)))
12	11	bieudv 1013	. . . . . 6 ⊢ (t = z → (∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y) ↔ ∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y)))
13	12	cbvralv 1333	. . . . 5 ⊢ (∀t ∈ x ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y) ↔ ∀z ∈ x ∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y))
14	9, 13	imbi12i 163	. . . 4 ⊢ ((∀t ∈ x ¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∀t ∈ x ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)) ↔ (∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → ∀z ∈ x ∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y)))
15		kmlem8.1	. . . . . . . . . . . 12 ⊢ A = {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))}
16	15	kmlem10 3589	. . . . . . . . . . 11 ⊢ (z ∈ x → (z ∩ ∪A) = (z ∖ ∪(x ∖ {z})))
17	16	ineq1d 1644	. . . . . . . . . 10 ⊢ (z ∈ x → ((z ∩ ∪A) ∩ y) = ((z ∖ ∪(x ∖ {z})) ∩ y))
18		in12 1651	. . . . . . . . . . 11 ⊢ (z ∩ (y ∩ ∪A)) = (y ∩ (z ∩ ∪A))
19		incom 1636	. . . . . . . . . . 11 ⊢ (y ∩ (z ∩ ∪A)) = ((z ∩ ∪A) ∩ y)
20	18, 19	eqtr 1119	. . . . . . . . . 10 ⊢ (z ∩ (y ∩ ∪A)) = ((z ∩ ∪A) ∩ y)
21	17, 20	syl5req 1137	. . . . . . . . 9 ⊢ (z ∈ x → ((z ∖ ∪(x ∖ {z})) ∩ y) = (z ∩ (y ∩ ∪A)))
22	21	eleq2d 1156	. . . . . . . 8 ⊢ (z ∈ x → (v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y) ↔ v ∈ (z ∩ (y ∩ ∪A))))
23	22	bieudv 1013	. . . . . . 7 ⊢ (z ∈ x → (∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y) ↔ ∃!v v ∈ (z ∩ (y ∩ ∪A))))
24		ax-1 3	. . . . . . 7 ⊢ (∃!v v ∈ (z ∩ (y ∩ ∪A)) → (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A))))
25	23, 24	syl6bi 187	. . . . . 6 ⊢ (z ∈ x → (∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y) → (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A)))))
26	25	r19.20i 1253	. . . . 5 ⊢ (∀z ∈ x ∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y) → ∀z ∈ x (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A))))
27	26	syl3 18	. . . 4 ⊢ ((∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → ∀z ∈ x ∃!v v ∈ ((z ∖ ∪(x ∖ {z})) ∩ y)) → (∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → ∀z ∈ x (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A)))))
28	14, 27	sylbi 174	. . 3 ⊢ ((∀t ∈ x ¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∀t ∈ x ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)) → (∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → ∀z ∈ x (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A)))))
29	28	com12 13	. 2 ⊢ (∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → ((∀t ∈ x ¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∀t ∈ x ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)) → ∀z ∈ x (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A)))))
30		raleq 1324	. . . . 5 ⊢ (A = {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} → (∀z ∈ A (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
31	15, 30	ax-mp 6	. . . 4 ⊢ (∀z ∈ A (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} (¬ z = ∅ → ∃!v v ∈ (z ∩ y)))
32		df-ral 1205	. . . 4 ⊢ (∀z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀z(z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
33		visset 1350	. . . . . . . . 9 ⊢ z ∈ V
34		cleq1 1107	. . . . . . . . . 10 ⊢ (u = z → (u = (t ∖ ∪(x ∖ {t})) ↔ z = (t ∖ ∪(x ∖ {t}))))
35	34	birexdv 1220	. . . . . . . . 9 ⊢ (u = z → (∃t ∈ x u = (t ∖ ∪(x ∖ {t})) ↔ ∃t ∈ x z = (t ∖ ∪(x ∖ {t}))))
36	33, 35	elab 1415	. . . . . . . 8 ⊢ (z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} ↔ ∃t ∈ x z = (t ∖ ∪(x ∖ {t})))
37	36	imbi1i 161	. . . . . . 7 ⊢ ((z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ (∃t ∈ x z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
38		r19.23v 1282	. . . . . . 7 ⊢ (∀t ∈ x (z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ (∃t ∈ x z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
39	37, 38	bitr4 154	. . . . . 6 ⊢ ((z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀t ∈ x (z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
40	39	bial 695	. . . . 5 ⊢ (∀z(z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀z∀t ∈ x (z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
41		ralcom4 1360	. . . . . 6 ⊢ (∀t ∈ x ∀z(z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀z∀t ∈ x (z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))))
42		visset 1350	. . . . . . . . 9 ⊢ t ∈ V
43		difexg 1703	. . . . . . . . 9 ⊢ (t ∈ V → (t ∖ ∪(x ∖ {t})) ∈ V)
44	42, 43	ax-mp 6	. . . . . . . 8 ⊢ (t ∖ ∪(x ∖ {t})) ∈ V
45		cleq1 1107	. . . . . . . . . 10 ⊢ (z = (t ∖ ∪(x ∖ {t})) → (z = ∅ ↔ (t ∖ ∪(x ∖ {t})) = ∅))
46	45	negbid 463	. . . . . . . . 9 ⊢ (z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ ↔ ¬ (t ∖ ∪(x ∖ {t})) = ∅))
47		ineq1 1638	. . . . . . . . . . 11 ⊢ (z = (t ∖ ∪(x ∖ {t})) → (z ∩ y) = ((t ∖ ∪(x ∖ {t})) ∩ y))
48	47	eleq2d 1156	. . . . . . . . . 10 ⊢ (z = (t ∖ ∪(x ∖ {t})) → (v ∈ (z ∩ y) ↔ v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
49	48	bieudv 1013	. . . . . . . . 9 ⊢ (z = (t ∖ ∪(x ∖ {t})) → (∃!v v ∈ (z ∩ y) ↔ ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
50	46, 49	imbi12d 474	. . . . . . . 8 ⊢ (z = (t ∖ ∪(x ∖ {t})) → ((¬ z = ∅ → ∃!v v ∈ (z ∩ y)) ↔ (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y))))
51	44, 50	ceqsalv 1364	. . . . . . 7 ⊢ (∀z(z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
52	51	biral 1223	. . . . . 6 ⊢ (∀t ∈ x ∀z(z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀t ∈ x (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
53	41, 52	bitr3 153	. . . . 5 ⊢ (∀z∀t ∈ x (z = (t ∖ ∪(x ∖ {t})) → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀t ∈ x (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
54	40, 53	bitr 151	. . . 4 ⊢ (∀z(z ∈ {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))} → (¬ z = ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀t ∈ x (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
55	31, 32, 54	3bitr 155	. . 3 ⊢ (∀z ∈ A (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀t ∈ x (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
56		r19.20 1251	. . 3 ⊢ (∀t ∈ x (¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)) → (∀t ∈ x ¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∀t ∈ x ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
57	55, 56	sylbi 174	. 2 ⊢ (∀z ∈ A (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) → (∀t ∈ x ¬ (t ∖ ∪(x ∖ {t})) = ∅ → ∀t ∈ x ∃!v v ∈ ((t ∖ ∪(x ∖ {t})) ∩ y)))
58	29, 57	syl5 22	1 ⊢ (∀z ∈ x ¬ (z ∖ ∪(x ∖ {z})) = ∅ → (∀z ∈ A (¬ z = ∅ → ∃!v v ∈ (z ∩ y)) → ∀z ∈ x (¬ z = ∅ → ∃!v v ∈ (z ∩ (y ∩ ∪A)))))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127  ∀wal 672   = weq 797   ∈ wel 803  ∃!weu 1007  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ∩ cin 1486  ∅c0 1707  {csn 1808  ∪cuni 1919

This theorem is referenced by:  kmlem12 3591

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-sn 1811  df-uni 1920  df-iun 1996

metamath.org