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 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
Assertion kmlem13 ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2 kmlem1 ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
3 raleq ⊢ ( 𝑥 = ℎ → ( ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
4 3 raleqbi1dv ⊢ ( 𝑥 = ℎ → ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
5 raleq ⊢ ( 𝑥 = ℎ → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
6 5 exbidv ⊢ ( 𝑥 = ℎ → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
7 4 6 imbi12d ⊢ ( 𝑥 = ℎ → ( ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) )
8 7 cbvalvw ⊢ ( ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
9 1 kmlem10 ⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
10 ineq2 ⊢ ( 𝑦 = 𝑔 → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑔 ) )
11 10 eleq2d ⊢ ( 𝑦 = 𝑔 → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) )
12 11 eubidv ⊢ ( 𝑦 = 𝑔 → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) )
13 12 imbi2d ⊢ ( 𝑦 = 𝑔 → ( ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) ) )
14 13 ralbidv ⊢ ( 𝑦 = 𝑔 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) ) )
15 14 cbvexvw ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) )
16 kmlem3 ⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
17 ralinexa ⊢ ( ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
18 17 rexbii ⊢ ( ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑣 ∈ 𝑧 ¬ ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
19 rexnal ⊢ ( ∃ 𝑣 ∈ 𝑧 ¬ ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
20 16 18 19 3bitri ⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
21 20 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∀ 𝑧 ∈ 𝑥 ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
22 ralnex ⊢ ( ∀ 𝑧 ∈ 𝑥 ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
23 21 22 bitri ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
24 1 kmlem12 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) ) )
25 vex ⊢ 𝑔 ∈ V
26 25 inex1 ⊢ ( 𝑔 ∩ ∪ 𝐴 ) ∈ V
27 ineq2 ⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) )
28 27 eleq2d ⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) )
29 28 eubidv ⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) )
30 29 imbi2d ⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) ) )
31 30 ralbidv ⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) ) )
32 26 31 spcev ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
33 24 32 syl6 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
34 33 exlimdv ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
35 34 com12 ⊢ ( ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
36 23 35 syl5bir ⊢ ( ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
37 15 36 sylbi ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
38 9 37 syl ⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
39 38 alrimiv ⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
40 8 39 sylbi ⊢ ( ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
41 2 40 syl ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
42 kmlem7 ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
43 42 imim1i ⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
44 biimt ⊢ ( 𝑧 ≠ ∅ → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
45 44 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
46 ralbi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
47 45 46 syl ⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
48 47 exbidv ⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
49 48 adantr ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
50 49 pm5.74i ⊢ ( ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
51 43 50 sylibr ⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
52 51 alimi ⊢ ( ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
53 41 52 impbii ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )