Metamath Proof Explorer

Theorem kmlem10

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

Ref Expression
Hypothesis kmlem9.1 ⊢ A = u | ∃ t ∈ x u = t ∖ ⋃ x ∖ t
Assertion kmlem10 ⊢ ∀ h ∀ z ∈ h ∀ w ∈ h z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ h φ → ∃ y ∀ z ∈ A φ

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢ A = u | ∃ t ∈ x u = t ∖ ⋃ x ∖ t
2 1 kmlem9 ⊢ ∀ z ∈ A ∀ w ∈ A z ≠ w → z ∩ w = ∅
3 vex ⊢ x ∈ V
4 3 abrexex ⊢ u | ∃ t ∈ x u = t ∖ ⋃ x ∖ t ∈ V
5 1 4 eqeltri ⊢ A ∈ V
6 raleq ⊢ h = A → ∀ w ∈ h z ≠ w → z ∩ w = ∅ ↔ ∀ w ∈ A z ≠ w → z ∩ w = ∅
7 6 raleqbi1dv ⊢ h = A → ∀ z ∈ h ∀ w ∈ h z ≠ w → z ∩ w = ∅ ↔ ∀ z ∈ A ∀ w ∈ A z ≠ w → z ∩ w = ∅
8 raleq ⊢ h = A → ∀ z ∈ h φ ↔ ∀ z ∈ A φ
9 8 exbidv ⊢ h = A → ∃ y ∀ z ∈ h φ ↔ ∃ y ∀ z ∈ A φ
10 7 9 imbi12d ⊢ h = A → ∀ z ∈ h ∀ w ∈ h z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ h φ ↔ ∀ z ∈ A ∀ w ∈ A z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ A φ
11 5 10 spcv ⊢ ∀ h ∀ z ∈ h ∀ w ∈ h z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ h φ → ∀ z ∈ A ∀ w ∈ A z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ A φ
12 2 11 mpi ⊢ ∀ h ∀ z ∈ h ∀ w ∈ h z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ h φ → ∃ y ∀ z ∈ A φ