This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
Assertion kmlem10 ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2 1 kmlem9 ⊢ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ )
3 vex ⊢ 𝑥 ∈ V
4 3 abrexex ⊢ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ∈ V
5 1 4 eqeltri ⊢ 𝐴 ∈ V
6 raleq ⊢ ( ℎ = 𝐴 → ( ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
7 6 raleqbi1dv ⊢ ( ℎ = 𝐴 → ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
8 raleq ⊢ ( ℎ = 𝐴 → ( ∀ 𝑧 ∈ ℎ 𝜑 ↔ ∀ 𝑧 ∈ 𝐴 𝜑 ) )
9 8 exbidv ⊢ ( ℎ = 𝐴 → ( ∃ 𝑦 ∀ 𝑧 ∈ ℎ 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 𝜑 ) )
10 7 9 imbi12d ⊢ ( ℎ = 𝐴 → ( ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ 𝜑 ) ↔ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 𝜑 ) ) )
11 5 10 spcv ⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ 𝜑 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 𝜑 ) )
12 2 11 mpi ⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 𝜑 )