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 ⊢ φ ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v
kmlem14.2 ⊢ ψ ↔ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
kmlem14.3 ⊢ χ ↔ ∀ z ∈ x ∃! v v ∈ z ∩ y
Assertion kmlem15 ⊢ ¬ y ∈ x ∧ χ ↔ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ

Proof

Step Hyp Ref Expression
1 kmlem14.1 ⊢ φ ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v
2 kmlem14.2 ⊢ ψ ↔ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
3 kmlem14.3 ⊢ χ ↔ ∀ z ∈ x ∃! v v ∈ z ∩ y
4 nfv ⊢ Ⅎ u v ∈ z ∩ y
5 4 eu1 ⊢ ∃! v v ∈ z ∩ y ↔ ∃ v v ∈ z ∩ y ∧ ∀ u u v v ∈ z ∩ y → v = u
6 elin ⊢ v ∈ z ∩ y ↔ v ∈ z ∧ v ∈ y
7 clelsb1 ⊢ u v v ∈ z ∩ y ↔ u ∈ z ∩ y
8 elin ⊢ u ∈ z ∩ y ↔ u ∈ z ∧ u ∈ y
9 7 8 bitri ⊢ u v v ∈ z ∩ y ↔ u ∈ z ∧ u ∈ y
10 equcom ⊢ v = u ↔ u = v
11 9 10 imbi12i ⊢ u v v ∈ z ∩ y → v = u ↔ u ∈ z ∧ u ∈ y → u = v
12 11 albii ⊢ ∀ u u v v ∈ z ∩ y → v = u ↔ ∀ u u ∈ z ∧ u ∈ y → u = v
13 6 12 anbi12i ⊢ v ∈ z ∩ y ∧ ∀ u u v v ∈ z ∩ y → v = u ↔ v ∈ z ∧ v ∈ y ∧ ∀ u u ∈ z ∧ u ∈ y → u = v
14 19.28v ⊢ ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v ↔ v ∈ z ∧ v ∈ y ∧ ∀ u u ∈ z ∧ u ∈ y → u = v
15 13 14 bitr4i ⊢ v ∈ z ∩ y ∧ ∀ u u v v ∈ z ∩ y → v = u ↔ ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
16 15 exbii ⊢ ∃ v v ∈ z ∩ y ∧ ∀ u u v v ∈ z ∩ y → v = u ↔ ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
17 5 16 bitri ⊢ ∃! v v ∈ z ∩ y ↔ ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
18 17 ralbii ⊢ ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ x ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
19 df-ral ⊢ ∀ z ∈ x ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v ↔ ∀ z z ∈ x → ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
20 2 albii ⊢ ∀ u ψ ↔ ∀ u z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
21 19.21v ⊢ ∀ u z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v ↔ z ∈ x → ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
22 20 21 bitri ⊢ ∀ u ψ ↔ z ∈ x → ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
23 22 exbii ⊢ ∃ v ∀ u ψ ↔ ∃ v z ∈ x → ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
24 19.37v ⊢ ∃ v z ∈ x → ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v ↔ z ∈ x → ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
25 23 24 bitri ⊢ ∃ v ∀ u ψ ↔ z ∈ x → ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
26 25 albii ⊢ ∀ z ∃ v ∀ u ψ ↔ ∀ z z ∈ x → ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
27 19 26 bitr4i ⊢ ∀ z ∈ x ∃ v ∀ u v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v ↔ ∀ z ∃ v ∀ u ψ
28 3 18 27 3bitri ⊢ χ ↔ ∀ z ∃ v ∀ u ψ
29 28 anbi2i ⊢ ¬ y ∈ x ∧ χ ↔ ¬ y ∈ x ∧ ∀ z ∃ v ∀ u ψ
30 19.28v ⊢ ∀ z ¬ y ∈ x ∧ ∃ v ∀ u ψ ↔ ¬ y ∈ x ∧ ∀ z ∃ v ∀ u ψ
31 19.28v ⊢ ∀ u ¬ y ∈ x ∧ ψ ↔ ¬ y ∈ x ∧ ∀ u ψ
32 31 exbii ⊢ ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∃ v ¬ y ∈ x ∧ ∀ u ψ
33 19.42v ⊢ ∃ v ¬ y ∈ x ∧ ∀ u ψ ↔ ¬ y ∈ x ∧ ∃ v ∀ u ψ
34 32 33 bitr2i ⊢ ¬ y ∈ x ∧ ∃ v ∀ u ψ ↔ ∃ v ∀ u ¬ y ∈ x ∧ ψ
35 34 albii ⊢ ∀ z ¬ y ∈ x ∧ ∃ v ∀ u ψ ↔ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
36 29 30 35 3bitr2i ⊢ ¬ y ∈ x ∧ χ ↔ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ