Metamath Proof Explorer

Theorem kmlem1

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

Ref Expression
Assertion kmlem1 ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x ψ → ∀ x ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x z ≠ ∅ → ψ

Proof

Step Hyp Ref Expression
1 vex ⊢ v ∈ V
2 1 rabex ⊢ u ∈ v | u ≠ ∅ ∈ V
3 raleq ⊢ x = u ∈ v | u ≠ ∅ → ∀ z ∈ x z ≠ ∅ ↔ ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅
4 raleq ⊢ x = u ∈ v | u ≠ ∅ → ∀ w ∈ x φ ↔ ∀ w ∈ u ∈ v | u ≠ ∅ φ
5 4 raleqbi1dv ⊢ x = u ∈ v | u ≠ ∅ → ∀ z ∈ x ∀ w ∈ x φ ↔ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ
6 3 5 anbi12d ⊢ x = u ∈ v | u ≠ ∅ → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ ↔ ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅ ∧ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ
7 raleq ⊢ x = u ∈ v | u ≠ ∅ → ∀ z ∈ x ψ ↔ ∀ z ∈ u ∈ v | u ≠ ∅ ψ
8 7 exbidv ⊢ x = u ∈ v | u ≠ ∅ → ∃ y ∀ z ∈ x ψ ↔ ∃ y ∀ z ∈ u ∈ v | u ≠ ∅ ψ
9 6 8 imbi12d ⊢ x = u ∈ v | u ≠ ∅ → ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x ψ ↔ ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅ ∧ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ → ∃ y ∀ z ∈ u ∈ v | u ≠ ∅ ψ
10 2 9 spcv ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x ψ → ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅ ∧ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ → ∃ y ∀ z ∈ u ∈ v | u ≠ ∅ ψ
11 10 alrimiv ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x ψ → ∀ v ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅ ∧ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ → ∃ y ∀ z ∈ u ∈ v | u ≠ ∅ ψ
12 elrabi ⊢ z ∈ u ∈ v | u ≠ ∅ → z ∈ v
13 elrabi ⊢ w ∈ u ∈ v | u ≠ ∅ → w ∈ v
14 13 imim1i ⊢ w ∈ v → φ → w ∈ u ∈ v | u ≠ ∅ → φ
15 14 ralimi2 ⊢ ∀ w ∈ v φ → ∀ w ∈ u ∈ v | u ≠ ∅ φ
16 12 15 imim12i ⊢ z ∈ v → ∀ w ∈ v φ → z ∈ u ∈ v | u ≠ ∅ → ∀ w ∈ u ∈ v | u ≠ ∅ φ
17 16 ralimi2 ⊢ ∀ z ∈ v ∀ w ∈ v φ → ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ
18 neeq1 ⊢ u = z → u ≠ ∅ ↔ z ≠ ∅
19 18 elrab ⊢ z ∈ u ∈ v | u ≠ ∅ ↔ z ∈ v ∧ z ≠ ∅
20 19 simprbi ⊢ z ∈ u ∈ v | u ≠ ∅ → z ≠ ∅
21 20 rgen ⊢ ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅
22 17 21 jctil ⊢ ∀ z ∈ v ∀ w ∈ v φ → ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅ ∧ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ
23 19 biimpri ⊢ z ∈ v ∧ z ≠ ∅ → z ∈ u ∈ v | u ≠ ∅
24 23 imim1i ⊢ z ∈ u ∈ v | u ≠ ∅ → ψ → z ∈ v ∧ z ≠ ∅ → ψ
25 24 expd ⊢ z ∈ u ∈ v | u ≠ ∅ → ψ → z ∈ v → z ≠ ∅ → ψ
26 25 ralimi2 ⊢ ∀ z ∈ u ∈ v | u ≠ ∅ ψ → ∀ z ∈ v z ≠ ∅ → ψ
27 26 eximi ⊢ ∃ y ∀ z ∈ u ∈ v | u ≠ ∅ ψ → ∃ y ∀ z ∈ v z ≠ ∅ → ψ
28 22 27 imim12i ⊢ ∀ z ∈ u ∈ v | u ≠ ∅ z ≠ ∅ ∧ ∀ z ∈ u ∈ v | u ≠ ∅ ∀ w ∈ u ∈ v | u ≠ ∅ φ → ∃ y ∀ z ∈ u ∈ v | u ≠ ∅ ψ → ∀ z ∈ v ∀ w ∈ v φ → ∃ y ∀ z ∈ v z ≠ ∅ → ψ
29 11 28 sylg ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x ψ → ∀ v ∀ z ∈ v ∀ w ∈ v φ → ∃ y ∀ z ∈ v z ≠ ∅ → ψ
30 raleq ⊢ v = x → ∀ w ∈ v φ ↔ ∀ w ∈ x φ
31 30 raleqbi1dv ⊢ v = x → ∀ z ∈ v ∀ w ∈ v φ ↔ ∀ z ∈ x ∀ w ∈ x φ
32 raleq ⊢ v = x → ∀ z ∈ v z ≠ ∅ → ψ ↔ ∀ z ∈ x z ≠ ∅ → ψ
33 32 exbidv ⊢ v = x → ∃ y ∀ z ∈ v z ≠ ∅ → ψ ↔ ∃ y ∀ z ∈ x z ≠ ∅ → ψ
34 31 33 imbi12d ⊢ v = x → ∀ z ∈ v ∀ w ∈ v φ → ∃ y ∀ z ∈ v z ≠ ∅ → ψ ↔ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x z ≠ ∅ → ψ
35 34 cbvalvw ⊢ ∀ v ∀ z ∈ v ∀ w ∈ v φ → ∃ y ∀ z ∈ v z ≠ ∅ → ψ ↔ ∀ x ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x z ≠ ∅ → ψ
36 29 35 sylib ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x ψ → ∀ x ∀ z ∈ x ∀ w ∈ x φ → ∃ y ∀ z ∈ x z ≠ ∅ → ψ