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

Metamath Proof Explorer

Theorem kmlem16

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

Ref Expression
Hypotheses kmlem14.1 ⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
kmlem14.2 ⊢ ( 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
kmlem14.3 ⊢ ( 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
Assertion kmlem16 ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 kmlem14.1 ⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
2 kmlem14.2 ⊢ ( 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
3 kmlem14.3 ⊢ ( 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
4 1 2 3 kmlem14 ⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
5 1 2 3 kmlem15 ⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )
7 4 6 orbi12i ⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
8 19.43 ⊢ ( ∃ 𝑦 ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
9 pm3.24 ⊢ ¬ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 )
10 simpl ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 )
11 10 sps ⊢ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 )
12 11 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 )
13 simpl ⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 )
14 13 sps ⊢ ( ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 )
15 14 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 )
16 12 15 anim12i ⊢ ( ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) )
17 9 16 mto ⊢ ¬ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )
18 19.33b ⊢ ( ¬ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( ∀ 𝑧 ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) )
19 17 18 ax-mp ⊢ ( ∀ 𝑧 ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
20 10 exlimiv ⊢ ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 )
21 13 exlimiv ⊢ ( ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 )
22 20 21 anim12i ⊢ ( ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) )
23 9 22 mto ⊢ ¬ ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )
24 19.33b ⊢ ( ¬ ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) )
25 23 24 ax-mp ⊢ ( ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
26 25 exbii ⊢ ( ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑣 ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
27 19.43 ⊢ ( ∃ 𝑣 ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
28 26 27 bitr2i ⊢ ( ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
29 28 albii ⊢ ( ∀ 𝑧 ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
30 19 29 bitr3i ⊢ ( ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
31 30 exbii ⊢ ( ∃ 𝑦 ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )
32 7 8 31 3bitr2i ⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )