Metamath Proof Explorer

Theorem kmlem14

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 kmlem14 ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ∃ y ∀ 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 neeq1 ⊢ z = y → z ≠ w ↔ y ≠ w
5 ineq1 ⊢ z = y → z ∩ w = y ∩ w
6 5 eleq2d ⊢ z = y → v ∈ z ∩ w ↔ v ∈ y ∩ w
7 4 6 anbi12d ⊢ z = y → z ≠ w ∧ v ∈ z ∩ w ↔ y ≠ w ∧ v ∈ y ∩ w
8 7 rexbidv ⊢ z = y → ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w
9 8 raleqbi1dv ⊢ z = y → ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w
10 9 cbvrexvw ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ∃ y ∈ x ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w
11 df-rex ⊢ ∃ y ∈ x ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ ∃ y y ∈ x ∧ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w
12 eleq1w ⊢ v = z → v ∈ y ∩ w ↔ z ∈ y ∩ w
13 12 anbi2d ⊢ v = z → y ≠ w ∧ v ∈ y ∩ w ↔ y ≠ w ∧ z ∈ y ∩ w
14 13 rexbidv ⊢ v = z → ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w
15 14 cbvralvw ⊢ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ ∀ z ∈ y ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w
16 df-ral ⊢ ∀ z ∈ y ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ ∀ z z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w
17 15 16 bitri ⊢ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ ∀ z z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w
18 17 anbi2i ⊢ y ∈ x ∧ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ y ∈ x ∧ ∀ z z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w
19 19.28v ⊢ ∀ z y ∈ x ∧ z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ y ∈ x ∧ ∀ z z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w
20 neeq2 ⊢ w = v → y ≠ w ↔ y ≠ v
21 ineq2 ⊢ w = v → y ∩ w = y ∩ v
22 21 eleq2d ⊢ w = v → z ∈ y ∩ w ↔ z ∈ y ∩ v
23 20 22 anbi12d ⊢ w = v → y ≠ w ∧ z ∈ y ∩ w ↔ y ≠ v ∧ z ∈ y ∩ v
24 23 cbvrexvw ⊢ ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ ∃ v ∈ x y ≠ v ∧ z ∈ y ∩ v
25 df-rex ⊢ ∃ v ∈ x y ≠ v ∧ z ∈ y ∩ v ↔ ∃ v v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
26 24 25 bitri ⊢ ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ ∃ v v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
27 26 imbi2i ⊢ z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ z ∈ y → ∃ v v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
28 19.37v ⊢ ∃ v z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v ↔ z ∈ y → ∃ v v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
29 27 28 bitr4i ⊢ z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ ∃ v z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
30 29 anbi2i ⊢ y ∈ x ∧ z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ y ∈ x ∧ ∃ v z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
31 19.42v ⊢ ∃ v y ∈ x ∧ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v ↔ y ∈ x ∧ ∃ v z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
32 19.3v ⊢ ∀ u y ∈ x ∧ φ ↔ y ∈ x ∧ φ
33 elin ⊢ z ∈ y ∩ v ↔ z ∈ y ∧ z ∈ v
34 33 baibr ⊢ z ∈ y → z ∈ v ↔ z ∈ y ∩ v
35 34 anbi2d ⊢ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v ↔ v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
36 anass ⊢ v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v ↔ v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
37 35 36 bitrdi ⊢ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v ↔ v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
38 37 pm5.74i ⊢ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
39 1 38 bitri ⊢ φ ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
40 39 anbi2i ⊢ y ∈ x ∧ φ ↔ y ∈ x ∧ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v
41 32 40 bitr2i ⊢ y ∈ x ∧ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v ↔ ∀ u y ∈ x ∧ φ
42 41 exbii ⊢ ∃ v y ∈ x ∧ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ y ∩ v ↔ ∃ v ∀ u y ∈ x ∧ φ
43 30 31 42 3bitr2i ⊢ y ∈ x ∧ z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ ∃ v ∀ u y ∈ x ∧ φ
44 43 albii ⊢ ∀ z y ∈ x ∧ z ∈ y → ∃ w ∈ x y ≠ w ∧ z ∈ y ∩ w ↔ ∀ z ∃ v ∀ u y ∈ x ∧ φ
45 18 19 44 3bitr2i ⊢ y ∈ x ∧ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ ∀ z ∃ v ∀ u y ∈ x ∧ φ
46 45 exbii ⊢ ∃ y y ∈ x ∧ ∀ v ∈ y ∃ w ∈ x y ≠ w ∧ v ∈ y ∩ w ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ
47 10 11 46 3bitri ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ