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 ∈ x u = t ∖ ⋃ x ∖ t
Assertion 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

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢ A = u | ∃ t ∈ x u = t ∖ ⋃ x ∖ t
2 kmlem1 ⊢ ∀ 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
3 raleq ⊢ x = h → ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ w ∈ h z ≠ w → z ∩ w = ∅
4 3 raleqbi1dv ⊢ x = h → ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ h ∀ w ∈ h z ≠ w → z ∩ w = ∅
5 raleq ⊢ x = h → ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∀ z ∈ h z ≠ ∅ → ∃! v v ∈ z ∩ y
6 5 exbidv ⊢ x = h → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∃ y ∀ z ∈ h z ≠ ∅ → ∃! v v ∈ z ∩ y
7 4 6 imbi12d ⊢ 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
8 7 cbvalvw ⊢ ∀ 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
9 1 kmlem10 ⊢ ∀ 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 ⊢ y = g → z ∩ y = z ∩ g
11 10 eleq2d ⊢ y = g → v ∈ z ∩ y ↔ v ∈ z ∩ g
12 11 eubidv ⊢ y = g → ∃! v v ∈ z ∩ y ↔ ∃! v v ∈ z ∩ g
13 12 imbi2d ⊢ y = g → z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ z ≠ ∅ → ∃! v v ∈ z ∩ g
14 13 ralbidv ⊢ y = g → ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ g
15 14 cbvexvw ⊢ ∃ y ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∃ g ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ g
16 kmlem3 ⊢ z ∖ ⋃ x ∖ z ≠ ∅ ↔ ∃ v ∈ z ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
17 ralinexa ⊢ ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w ↔ ¬ ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
18 17 rexbii ⊢ ∃ v ∈ z ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w ↔ ∃ v ∈ z ¬ ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
19 rexnal ⊢ ∃ v ∈ z ¬ ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ¬ ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
20 16 18 19 3bitri ⊢ z ∖ ⋃ x ∖ z ≠ ∅ ↔ ¬ ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
21 20 ralbii ⊢ ∀ z ∈ x z ∖ ⋃ x ∖ z ≠ ∅ ↔ ∀ z ∈ x ¬ ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
22 ralnex ⊢ ∀ z ∈ x ¬ ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ¬ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
23 21 22 bitri ⊢ ∀ z ∈ x z ∖ ⋃ x ∖ z ≠ ∅ ↔ ¬ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w
24 1 kmlem12 ⊢ ∀ z ∈ x z ∖ ⋃ x ∖ z ≠ ∅ → ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ g → ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ 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 → ∃! v v ∈ z ∩ y ↔ ∃! v v ∈ z ∩ g ∩ ⋃ A
30 29 imbi2d ⊢ y = g ∩ ⋃ A → z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ z ≠ ∅ → ∃! v v ∈ z ∩ g ∩ ⋃ A
31 30 ralbidv ⊢ y = g ∩ ⋃ A → ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ g ∩ ⋃ A
32 26 31 spcev ⊢ ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ g ∩ ⋃ A → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
33 24 32 syl6 ⊢ ∀ z ∈ x z ∖ ⋃ x ∖ z ≠ ∅ → ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ g → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
34 33 exlimdv ⊢ ∀ z ∈ x z ∖ ⋃ x ∖ z ≠ ∅ → ∃ g ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ g → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
35 34 com12 ⊢ ∃ g ∀ z ∈ A z ≠ ∅ → ∃! v v ∈ z ∩ g → ∀ z ∈ x z ∖ ⋃ x ∖ z ≠ ∅ → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
36 23 35 syl5bir ⊢ ∃ 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 ⊢ ∃ 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 ⊢ ∀ 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 alrimiv ⊢ ∀ 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 8 39 sylbi ⊢ ∀ 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 2 40 syl ⊢ ∀ 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 ⊢ ∀ 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 ⊢ ¬ ∃ 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 ⊢ z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ z ≠ ∅ → ∃! v v ∈ z ∩ y
45 44 ralimi ⊢ ∀ z ∈ x z ≠ ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ z ≠ ∅ → ∃! v v ∈ z ∩ y
46 ralbi ⊢ ∀ 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 ⊢ ∀ z ∈ x z ≠ ∅ → ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
48 47 exbidv ⊢ ∀ z ∈ x z ≠ ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
49 48 adantr ⊢ ∀ 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 ⊢ ∀ 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 ⊢ ¬ ∃ 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 alimi ⊢ ∀ 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 impbii ⊢ ∀ 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