This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kmlem8

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

Ref Expression
Assertion kmlem8 ( ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 ralnex ⊢ ( ∀ 𝑧 ∈ 𝑢 ¬ ∀ 𝑤 ∈ 𝑧 𝜓 ↔ ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 )
2 df-rex ⊢ ( ∃ 𝑤 ∈ 𝑧 ¬ 𝜓 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ¬ 𝜓 ) )
3 rexnal ⊢ ( ∃ 𝑤 ∈ 𝑧 ¬ 𝜓 ↔ ¬ ∀ 𝑤 ∈ 𝑧 𝜓 )
4 2 3 bitr3i ⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ¬ 𝜓 ) ↔ ¬ ∀ 𝑤 ∈ 𝑧 𝜓 )
5 exsimpl ⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ¬ 𝜓 ) → ∃ 𝑤 𝑤 ∈ 𝑧 )
6 n0 ⊢ ( 𝑧 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑧 )
7 5 6 sylibr ⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ¬ 𝜓 ) → 𝑧 ≠ ∅ )
8 4 7 sylbir ⊢ ( ¬ ∀ 𝑤 ∈ 𝑧 𝜓 → 𝑧 ≠ ∅ )
9 8 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑢 ¬ ∀ 𝑤 ∈ 𝑧 𝜓 → ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ )
10 1 9 sylbir ⊢ ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ )
11 kmlem2 ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
12 biimt ⊢ ( 𝑧 ≠ ∅ → ( ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
13 12 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ → ∀ 𝑧 ∈ 𝑢 ( ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
14 ralbi ⊢ ( ∀ 𝑧 ∈ 𝑢 ( ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
15 13 14 syl ⊢ ( ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ → ( ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
16 15 anbi2d ⊢ ( ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ → ( ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) )
17 16 exbidv ⊢ ( ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) )
18 11 17 bitr4id ⊢ ( ∀ 𝑧 ∈ 𝑢 𝑧 ≠ ∅ → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
19 10 18 syl ⊢ ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
20 19 pm5.74i ⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
21 pm4.64 ⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
22 20 21 bitri ⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑢 ( 𝑧 ≠ ∅ → ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑧 𝜓 ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑢 ∧ ∀ 𝑧 ∈ 𝑢 ∃! 𝑤 𝑤 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )