Metamath Proof Explorer

Theorem kmlem2

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion kmlem2 ⊢ ∃ y ∀ z ∈ x φ → ∃! w w ∈ z ∩ y ↔ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y

Proof

Step Hyp Ref Expression
1 ineq2 ⊢ y = v → z ∩ y = z ∩ v
2 1 eleq2d ⊢ y = v → w ∈ z ∩ y ↔ w ∈ z ∩ v
3 2 eubidv ⊢ y = v → ∃! w w ∈ z ∩ y ↔ ∃! w w ∈ z ∩ v
4 3 imbi2d ⊢ y = v → φ → ∃! w w ∈ z ∩ y ↔ φ → ∃! w w ∈ z ∩ v
5 4 ralbidv ⊢ y = v → ∀ z ∈ x φ → ∃! w w ∈ z ∩ y ↔ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v
6 5 cbvexvw ⊢ ∃ y ∀ z ∈ x φ → ∃! w w ∈ z ∩ y ↔ ∃ v ∀ z ∈ x φ → ∃! w w ∈ z ∩ v
7 indi ⊢ z ∩ v ∪ u = z ∩ v ∪ z ∩ u
8 elssuni ⊢ z ∈ x → z ⊆ ⋃ x
9 8 ssneld ⊢ z ∈ x → ¬ u ∈ ⋃ x → ¬ u ∈ z
10 disjsn ⊢ z ∩ u = ∅ ↔ ¬ u ∈ z
11 9 10 syl6ibr ⊢ z ∈ x → ¬ u ∈ ⋃ x → z ∩ u = ∅
12 11 impcom ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → z ∩ u = ∅
13 12 uneq2d ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → z ∩ v ∪ z ∩ u = z ∩ v ∪ ∅
14 un0 ⊢ z ∩ v ∪ ∅ = z ∩ v
15 13 14 eqtrdi ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → z ∩ v ∪ z ∩ u = z ∩ v
16 7 15 syl5req ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → z ∩ v = z ∩ v ∪ u
17 16 eleq2d ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → w ∈ z ∩ v ↔ w ∈ z ∩ v ∪ u
18 17 eubidv ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → ∃! w w ∈ z ∩ v ↔ ∃! w w ∈ z ∩ v ∪ u
19 18 imbi2d ⊢ ¬ u ∈ ⋃ x ∧ z ∈ x → φ → ∃! w w ∈ z ∩ v ↔ φ → ∃! w w ∈ z ∩ v ∪ u
20 19 ralbidva ⊢ ¬ u ∈ ⋃ x → ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ↔ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u
21 vsnid ⊢ u ∈ u
22 21 olci ⊢ u ∈ v ∨ u ∈ u
23 elun ⊢ u ∈ v ∪ u ↔ u ∈ v ∨ u ∈ u
24 22 23 mpbir ⊢ u ∈ v ∪ u
25 elssuni ⊢ v ∪ u ∈ x → v ∪ u ⊆ ⋃ x
26 25 sseld ⊢ v ∪ u ∈ x → u ∈ v ∪ u → u ∈ ⋃ x
27 24 26 mpi ⊢ v ∪ u ∈ x → u ∈ ⋃ x
28 27 con3i ⊢ ¬ u ∈ ⋃ x → ¬ v ∪ u ∈ x
29 28 biantrurd ⊢ ¬ u ∈ ⋃ x → ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u ↔ ¬ v ∪ u ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u
30 20 29 bitrd ⊢ ¬ u ∈ ⋃ x → ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ↔ ¬ v ∪ u ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u
31 vex ⊢ v ∈ V
32 snex ⊢ u ∈ V
33 31 32 unex ⊢ v ∪ u ∈ V
34 eleq1 ⊢ y = v ∪ u → y ∈ x ↔ v ∪ u ∈ x
35 34 notbid ⊢ y = v ∪ u → ¬ y ∈ x ↔ ¬ v ∪ u ∈ x
36 ineq2 ⊢ y = v ∪ u → z ∩ y = z ∩ v ∪ u
37 36 eleq2d ⊢ y = v ∪ u → w ∈ z ∩ y ↔ w ∈ z ∩ v ∪ u
38 37 eubidv ⊢ y = v ∪ u → ∃! w w ∈ z ∩ y ↔ ∃! w w ∈ z ∩ v ∪ u
39 38 imbi2d ⊢ y = v ∪ u → φ → ∃! w w ∈ z ∩ y ↔ φ → ∃! w w ∈ z ∩ v ∪ u
40 39 ralbidv ⊢ y = v ∪ u → ∀ z ∈ x φ → ∃! w w ∈ z ∩ y ↔ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u
41 35 40 anbi12d ⊢ y = v ∪ u → ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y ↔ ¬ v ∪ u ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u
42 33 41 spcev ⊢ ¬ v ∪ u ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v ∪ u → ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y
43 30 42 syl6bi ⊢ ¬ u ∈ ⋃ x → ∀ z ∈ x φ → ∃! w w ∈ z ∩ v → ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y
44 vuniex ⊢ ⋃ x ∈ V
45 eleq2 ⊢ y = ⋃ x → u ∈ y ↔ u ∈ ⋃ x
46 45 notbid ⊢ y = ⋃ x → ¬ u ∈ y ↔ ¬ u ∈ ⋃ x
47 46 exbidv ⊢ y = ⋃ x → ∃ u ¬ u ∈ y ↔ ∃ u ¬ u ∈ ⋃ x
48 nalset ⊢ ¬ ∃ y ∀ u u ∈ y
49 alexn ⊢ ∀ y ∃ u ¬ u ∈ y ↔ ¬ ∃ y ∀ u u ∈ y
50 48 49 mpbir ⊢ ∀ y ∃ u ¬ u ∈ y
51 50 spi ⊢ ∃ u ¬ u ∈ y
52 44 47 51 vtocl ⊢ ∃ u ¬ u ∈ ⋃ x
53 43 52 exlimiiv ⊢ ∀ z ∈ x φ → ∃! w w ∈ z ∩ v → ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y
54 53 exlimiv ⊢ ∃ v ∀ z ∈ x φ → ∃! w w ∈ z ∩ v → ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y
55 6 54 sylbi ⊢ ∃ y ∀ z ∈ x φ → ∃! w w ∈ z ∩ y → ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y
56 exsimpr ⊢ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y → ∃ y ∀ z ∈ x φ → ∃! w w ∈ z ∩ y
57 55 56 impbii ⊢ ∃ y ∀ z ∈ x φ → ∃! w w ∈ z ∩ y ↔ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x φ → ∃! w w ∈ z ∩ y