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	⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 𝜑 )