Theorem kmlem13 4757

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

Hypothesis

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

Assertion

Ref	Expression
kmlem13	⊢ (∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) ↔ ∀x(¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))

Distinct variable groups:   x,y,z,w,v,u,t   y,A,z,w,v

Proof of Theorem kmlem13

Step	Hyp	Ref	Expression
1		kmlem1 4745	. . 3 ⊢ (∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) → ∀x(∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
2		raleq1 1783	. . . . . . 7 ⊢ (x = h → (∀w ∈ x (z ≠ w → (z ∩ w) = ∅) ↔ ∀w ∈ h (z ≠ w → (z ∩ w) = ∅)))
3	2	raleqd 1788	. . . . . 6 ⊢ (x = h → (∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅) ↔ ∀z ∈ h ∀w ∈ h (z ≠ w → (z ∩ w) = ∅)))
4		raleq1 1783	. . . . . . 7 ⊢ (x = h → (∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
5	4	exbidv 1277	. . . . . 6 ⊢ (x = h → (∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∃y∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
6	3, 5	imbi12d 625	. . . . 5 ⊢ (x = h → ((∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) ↔ (∀z ∈ h ∀w ∈ h (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y)))))
7	6	cbvalv 1312	. . . 4 ⊢ (∀x(∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) ↔ ∀h(∀z ∈ h ∀w ∈ h (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
8		kmlem9.1	. . . . . . 7 ⊢ A = {u∣∃t ∈ x u = (t ∖ ∪(x ∖ {t}))}
9	8	kmlem10 4754	. . . . . 6 ⊢ (∀h(∀z ∈ h ∀w ∈ h (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → ∃y∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ y)))
10		ineq2 2207	. . . . . . . . . . . 12 ⊢ (y = g → (z ∩ y) = (z ∩ g))
11	10	eleq2d 1538	. . . . . . . . . . 11 ⊢ (y = g → (v ∈ (z ∩ y) ↔ v ∈ (z ∩ g)))
12	11	eubidv 1384	. . . . . . . . . 10 ⊢ (y = g → (∃!v v ∈ (z ∩ y) ↔ ∃!v v ∈ (z ∩ g)))
13	12	imbi2d 611	. . . . . . . . 9 ⊢ (y = g → ((z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ (z ≠ ∅ → ∃!v v ∈ (z ∩ g))))
14	13	ralbidv 1660	. . . . . . . 8 ⊢ (y = g → (∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g))))
15	14	cbvexv 1313	. . . . . . 7 ⊢ (∃y∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∃g∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g)))
16	8	kmlem12 4756	. . . . . . . . . . 11 ⊢ (∀z ∈ x (z ∖ ∪(x ∖ {z})) ≠ ∅ → (∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g)) → ∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ (g ∩ ∪A)))))
17		visset 1809	. . . . . . . . . . . . 13 ⊢ g ∈ V
18	17	inex1 2711	. . . . . . . . . . . 12 ⊢ (g ∩ ∪A) ∈ V
19		ineq2 2207	. . . . . . . . . . . . . . . 16 ⊢ (y = (g ∩ ∪A) → (z ∩ y) = (z ∩ (g ∩ ∪A)))
20	19	eleq2d 1538	. . . . . . . . . . . . . . 15 ⊢ (y = (g ∩ ∪A) → (v ∈ (z ∩ y) ↔ v ∈ (z ∩ (g ∩ ∪A))))
21	20	eubidv 1384	. . . . . . . . . . . . . 14 ⊢ (y = (g ∩ ∪A) → (∃!v v ∈ (z ∩ y) ↔ ∃!v v ∈ (z ∩ (g ∩ ∪A))))
22	21	imbi2d 611	. . . . . . . . . . . . 13 ⊢ (y = (g ∩ ∪A) → ((z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ (z ≠ ∅ → ∃!v v ∈ (z ∩ (g ∩ ∪A)))))
23	22	ralbidv 1660	. . . . . . . . . . . 12 ⊢ (y = (g ∩ ∪A) → (∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y)) ↔ ∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ (g ∩ ∪A)))))
24	18, 23	cla4ev 1865	. . . . . . . . . . 11 ⊢ (∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ (g ∩ ∪A))) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y)))
25	16, 24	syl6 22	. . . . . . . . . 10 ⊢ (∀z ∈ x (z ∖ ∪(x ∖ {z})) ≠ ∅ → (∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
26	25	19.23adv 1212	. . . . . . . . 9 ⊢ (∀z ∈ x (z ∖ ∪(x ∖ {z})) ≠ ∅ → (∃g∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
27	26	com12 11	. . . . . . . 8 ⊢ (∃g∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g)) → (∀z ∈ x (z ∖ ∪(x ∖ {z})) ≠ ∅ → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
28		kmlem3 4747	. . . . . . . . . . 11 ⊢ ((z ∖ ∪(x ∖ {z})) ≠ ∅ ↔ ∃v ∈ z ∀w ∈ x (z ≠ w → ¬ v ∈ (z ∩ w)))
29		ralinexa 1680	. . . . . . . . . . . 12 ⊢ (∀w ∈ x (z ≠ w → ¬ v ∈ (z ∩ w)) ↔ ¬ ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
30	29	rexbii 1665	. . . . . . . . . . 11 ⊢ (∃v ∈ z ∀w ∈ x (z ≠ w → ¬ v ∈ (z ∩ w)) ↔ ∃v ∈ z ¬ ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
31		rexnal 1651	. . . . . . . . . . 11 ⊢ (∃v ∈ z ¬ ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) ↔ ¬ ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
32	28, 30, 31	3bitr 177	. . . . . . . . . 10 ⊢ ((z ∖ ∪(x ∖ {z})) ≠ ∅ ↔ ¬ ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
33	32	ralbii 1664	. . . . . . . . 9 ⊢ (∀z ∈ x (z ∖ ∪(x ∖ {z})) ≠ ∅ ↔ ∀z ∈ x ¬ ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
34		ralnex 1650	. . . . . . . . 9 ⊢ (∀z ∈ x ¬ ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) ↔ ¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
35	33, 34	bitr 173	. . . . . . . 8 ⊢ (∀z ∈ x (z ∖ ∪(x ∖ {z})) ≠ ∅ ↔ ¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
36	27, 35	syl5ibr 207	. . . . . . 7 ⊢ (∃g∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ g)) → (¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
37	15, 36	sylbi 199	. . . . . 6 ⊢ (∃y∀z ∈ A (z ≠ ∅ → ∃!v v ∈ (z ∩ y)) → (¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
38	9, 37	syl 10	. . . . 5 ⊢ (∀h(∀z ∈ h ∀w ∈ h (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → (¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
39	38	19.21aiv 1284	. . . 4 ⊢ (∀h(∀z ∈ h ∀w ∈ h (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ h (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → ∀x(¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
40	7, 39	sylbi 199	. . 3 ⊢ (∀x(∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → ∀x(¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
41	1, 40	syl 10	. 2 ⊢ (∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) → ∀x(¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
42		kmlem7 4751	. . . . 5 ⊢ ((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)))
43	42	imim1i 16	. . . 4 ⊢ ((¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → ((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
44		biimt 730	. . . . . . . . 9 ⊢ (z ≠ ∅ → (∃!v v ∈ (z ∩ y) ↔ (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
45	44	r19.20si 1703	. . . . . . . 8 ⊢ (∀z ∈ x z ≠ ∅ → ∀z ∈ x (∃!v v ∈ (z ∩ y) ↔ (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
46		r19.15 1750	. . . . . . . 8 ⊢ (∀z ∈ x (∃!v v ∈ (z ∩ y) ↔ (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → (∀z ∈ x ∃!v v ∈ (z ∩ y) ↔ ∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
47	45, 46	syl 10	. . . . . . 7 ⊢ (∀z ∈ x z ≠ ∅ → (∀z ∈ x ∃!v v ∈ (z ∩ y) ↔ ∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
48	47	exbidv 1277	. . . . . 6 ⊢ (∀z ∈ x z ≠ ∅ → (∃y∀z ∈ x ∃!v v ∈ (z ∩ y) ↔ ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
49	48	adantr 389	. . . . 5 ⊢ ((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → (∃y∀z ∈ x ∃!v v ∈ (z ∩ y) ↔ ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
50	49	pm5.74i 583	. . . 4 ⊢ (((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) ↔ ((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))
51	43, 50	sylibr 200	. . 3 ⊢ ((¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → ((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
52	51	19.20i 990	. 2 ⊢ (∀x(¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))) → ∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
53	41, 52	impbi 157	1 ⊢ (∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) ↔ ∀x(¬ ∃z ∈ x ∀v ∈ z ∃w ∈ x (z ≠ w ⋀ v ∈ (z ∩ w)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!v v ∈ (z ∩ y))))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  ∃!weu 1378  {cab 1461   ≠ wne 1582  ∀wral 1642  ∃wrex 1643   ∖ cdif 2040   ∩ cin 2042  ∅c0 2276  {csn 2405  ∪cuni 2498

This theorem is referenced by:  aceqkm 4761

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-rab 1649  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-iun 2563  df-br 2615  df-opab 2662  df-id 2830  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fv 3193

Copyright terms: Public domain