Metamath Proof Explorer

Theorem kmlem13

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 5-Apr-2004)

Ref Expression
Hypothesis kmlem9.1 ⊢A=u|∃t∈xu=t∖⋃x∖t
Assertion kmlem13 ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢A=u|∃t∈xu=t∖⋃x∖t
2 kmlem1 ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y→∀x∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈xz≠∅→∃!vv∈z∩y
3 raleq ⊢x=h→∀w∈xz≠w→z∩w=∅↔∀w∈hz≠w→z∩w=∅
4 3 raleqbi1dv ⊢x=h→∀z∈x∀w∈xz≠w→z∩w=∅↔∀z∈h∀w∈hz≠w→z∩w=∅
5 raleq ⊢x=h→∀z∈xz≠∅→∃!vv∈z∩y↔∀z∈hz≠∅→∃!vv∈z∩y
6 5 exbidv ⊢x=h→∃y∀z∈xz≠∅→∃!vv∈z∩y↔∃y∀z∈hz≠∅→∃!vv∈z∩y
7 4 6 imbi12d ⊢x=h→∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈xz≠∅→∃!vv∈z∩y↔∀z∈h∀w∈hz≠w→z∩w=∅→∃y∀z∈hz≠∅→∃!vv∈z∩y
8 7 cbvalvw ⊢∀x∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈xz≠∅→∃!vv∈z∩y↔∀h∀z∈h∀w∈hz≠w→z∩w=∅→∃y∀z∈hz≠∅→∃!vv∈z∩y
9 1 kmlem10 ⊢∀h∀z∈h∀w∈hz≠w→z∩w=∅→∃y∀z∈hz≠∅→∃!vv∈z∩y→∃y∀z∈Az≠∅→∃!vv∈z∩y
10 ineq2 ⊢y=g→z∩y=z∩g
11 10 eleq2d ⊢y=g→v∈z∩y↔v∈z∩g
12 11 eubidv ⊢y=g→∃!vv∈z∩y↔∃!vv∈z∩g
13 12 imbi2d ⊢y=g→z≠∅→∃!vv∈z∩y↔z≠∅→∃!vv∈z∩g
14 13 ralbidv ⊢y=g→∀z∈Az≠∅→∃!vv∈z∩y↔∀z∈Az≠∅→∃!vv∈z∩g
15 14 cbvexvw ⊢∃y∀z∈Az≠∅→∃!vv∈z∩y↔∃g∀z∈Az≠∅→∃!vv∈z∩g
16 kmlem3 ⊢z∖⋃x∖z≠∅↔∃v∈z∀w∈xz≠w→¬v∈z∩w
17 ralinexa ⊢∀w∈xz≠w→¬v∈z∩w↔¬∃w∈xz≠w∧v∈z∩w
18 17 rexbii ⊢∃v∈z∀w∈xz≠w→¬v∈z∩w↔∃v∈z¬∃w∈xz≠w∧v∈z∩w
19 rexnal ⊢∃v∈z¬∃w∈xz≠w∧v∈z∩w↔¬∀v∈z∃w∈xz≠w∧v∈z∩w
20 16 18 19 3bitri ⊢z∖⋃x∖z≠∅↔¬∀v∈z∃w∈xz≠w∧v∈z∩w
21 20 ralbii ⊢∀z∈xz∖⋃x∖z≠∅↔∀z∈x¬∀v∈z∃w∈xz≠w∧v∈z∩w
22 ralnex ⊢∀z∈x¬∀v∈z∃w∈xz≠w∧v∈z∩w↔¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w
23 21 22 bitri ⊢∀z∈xz∖⋃x∖z≠∅↔¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w
24 1 kmlem12 ⊢∀z∈xz∖⋃x∖z≠∅→∀z∈Az≠∅→∃!vv∈z∩g→∀z∈xz≠∅→∃!vv∈z∩g∩⋃A
25 vex ⊢g∈V
26 25 inex1 ⊢g∩⋃A∈V
27 ineq2 ⊢y=g∩⋃A→z∩y=z∩g∩⋃A
28 27 eleq2d ⊢y=g∩⋃A→v∈z∩y↔v∈z∩g∩⋃A
29 28 eubidv ⊢y=g∩⋃A→∃!vv∈z∩y↔∃!vv∈z∩g∩⋃A
30 29 imbi2d ⊢y=g∩⋃A→z≠∅→∃!vv∈z∩y↔z≠∅→∃!vv∈z∩g∩⋃A
31 30 ralbidv ⊢y=g∩⋃A→∀z∈xz≠∅→∃!vv∈z∩y↔∀z∈xz≠∅→∃!vv∈z∩g∩⋃A
32 26 31 spcev ⊢∀z∈xz≠∅→∃!vv∈z∩g∩⋃A→∃y∀z∈xz≠∅→∃!vv∈z∩y
33 24 32 syl6 ⊢∀z∈xz∖⋃x∖z≠∅→∀z∈Az≠∅→∃!vv∈z∩g→∃y∀z∈xz≠∅→∃!vv∈z∩y
34 33 exlimdv ⊢∀z∈xz∖⋃x∖z≠∅→∃g∀z∈Az≠∅→∃!vv∈z∩g→∃y∀z∈xz≠∅→∃!vv∈z∩y
35 34 com12 ⊢∃g∀z∈Az≠∅→∃!vv∈z∩g→∀z∈xz∖⋃x∖z≠∅→∃y∀z∈xz≠∅→∃!vv∈z∩y
36 23 35 biimtrrid ⊢∃g∀z∈Az≠∅→∃!vv∈z∩g→¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
37 15 36 sylbi ⊢∃y∀z∈Az≠∅→∃!vv∈z∩y→¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
38 9 37 syl ⊢∀h∀z∈h∀w∈hz≠w→z∩w=∅→∃y∀z∈hz≠∅→∃!vv∈z∩y→¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
39 38 alrimiv ⊢∀h∀z∈h∀w∈hz≠w→z∩w=∅→∃y∀z∈hz≠∅→∃!vv∈z∩y→∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
40 8 39 sylbi ⊢∀x∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈xz≠∅→∃!vv∈z∩y→∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
41 2 40 syl ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y→∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
42 kmlem7 ⊢∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w
43 42 imim1i ⊢¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y→∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈xz≠∅→∃!vv∈z∩y
44 biimt ⊢z≠∅→∃!vv∈z∩y↔z≠∅→∃!vv∈z∩y
45 44 ralimi ⊢∀z∈xz≠∅→∀z∈x∃!vv∈z∩y↔z≠∅→∃!vv∈z∩y
46 ralbi ⊢∀z∈x∃!vv∈z∩y↔z≠∅→∃!vv∈z∩y→∀z∈x∃!vv∈z∩y↔∀z∈xz≠∅→∃!vv∈z∩y
47 45 46 syl ⊢∀z∈xz≠∅→∀z∈x∃!vv∈z∩y↔∀z∈xz≠∅→∃!vv∈z∩y
48 47 exbidv ⊢∀z∈xz≠∅→∃y∀z∈x∃!vv∈z∩y↔∃y∀z∈xz≠∅→∃!vv∈z∩y
49 48 adantr ⊢∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∃y∀z∈xz≠∅→∃!vv∈z∩y
50 49 pm5.74i ⊢∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈xz≠∅→∃!vv∈z∩y
51 43 50 sylibr ⊢¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y→∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
52 51 alimi ⊢∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y→∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
53 41 52 impbii ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y