Metamath Proof Explorer

Theorem kmlem15

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

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

Proof

Step Hyp Ref Expression
1 kmlem14.1 ⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
2 kmlem14.2 ⊢ ( 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
3 kmlem14.3 ⊢ ( 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
4 nfv ⊢ Ⅎ 𝑢 𝑣 ∈ ( 𝑧 ∩ 𝑦 )
5 4 eu1 ⊢ ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ∧ ∀ 𝑢 ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → 𝑣 = 𝑢 ) ) )
6 elin ⊢ ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) )
7 clelsb1 ⊢ ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑢 ∈ ( 𝑧 ∩ 𝑦 ) )
8 elin ⊢ ( 𝑢 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) )
9 7 8 bitri ⊢ ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) )
10 equcom ⊢ ( 𝑣 = 𝑢 ↔ 𝑢 = 𝑣 )
11 9 10 imbi12i ⊢ ( ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → 𝑣 = 𝑢 ) ↔ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) )
12 11 albii ⊢ ( ∀ 𝑢 ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → 𝑣 = 𝑢 ) ↔ ∀ 𝑢 ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) )
13 6 12 anbi12i ⊢ ( ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ∧ ∀ 𝑢 ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → 𝑣 = 𝑢 ) ) ↔ ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ∀ 𝑢 ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
14 19.28v ⊢ ( ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ↔ ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ∀ 𝑢 ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
15 13 14 bitr4i ⊢ ( ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ∧ ∀ 𝑢 ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → 𝑣 = 𝑢 ) ) ↔ ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
16 15 exbii ⊢ ( ∃ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ∧ ∀ 𝑢 ( [ 𝑢 / 𝑣 ] 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) → 𝑣 = 𝑢 ) ) ↔ ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
17 5 16 bitri ⊢ ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
18 17 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
19 df-ral ⊢ ( ∀ 𝑧 ∈ 𝑥 ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
20 2 albii ⊢ ( ∀ 𝑢 𝜓 ↔ ∀ 𝑢 ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
21 19.21v ⊢ ( ∀ 𝑢 ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ↔ ( 𝑧 ∈ 𝑥 → ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
22 20 21 bitri ⊢ ( ∀ 𝑢 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
23 22 exbii ⊢ ( ∃ 𝑣 ∀ 𝑢 𝜓 ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑥 → ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
24 19.37v ⊢ ( ∃ 𝑣 ( 𝑧 ∈ 𝑥 → ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ↔ ( 𝑧 ∈ 𝑥 → ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
25 23 24 bitri ⊢ ( ∃ 𝑣 ∀ 𝑢 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
26 25 albii ⊢ ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 𝜓 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
27 19 26 bitr4i ⊢ ( ∀ 𝑧 ∈ 𝑥 ∃ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 𝜓 )
28 3 18 27 3bitri ⊢ ( 𝜒 ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 𝜓 )
29 28 anbi2i ⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ↔ ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 𝜓 ) )
30 19.28v ⊢ ( ∀ 𝑧 ( ¬ 𝑦 ∈ 𝑥 ∧ ∃ 𝑣 ∀ 𝑢 𝜓 ) ↔ ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 𝜓 ) )
31 19.28v ⊢ ( ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ↔ ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑢 𝜓 ) )
32 31 exbii ⊢ ( ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ↔ ∃ 𝑣 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑢 𝜓 ) )
33 19.42v ⊢ ( ∃ 𝑣 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑢 𝜓 ) ↔ ( ¬ 𝑦 ∈ 𝑥 ∧ ∃ 𝑣 ∀ 𝑢 𝜓 ) )
34 32 33 bitr2i ⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ ∃ 𝑣 ∀ 𝑢 𝜓 ) ↔ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )
35 34 albii ⊢ ( ∀ 𝑧 ( ¬ 𝑦 ∈ 𝑥 ∧ ∃ 𝑣 ∀ 𝑢 𝜓 ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )
36 29 30 35 3bitr2i ⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) )