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 ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝜑 → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )

Proof

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