Theorem dfttc4lem1

Description: Lemma for dfttc4 . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Hypotheses	dfttc4lem1.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }
	dfttc4lem1.2	⊢ 𝐶 ∈ V
	dfttc4lem1.3	⊢ 𝐷 ∈ V
Assertion	dfttc4lem1	⊢ ( ( ( 𝐴 ∩ 𝐶 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐶 ( ( 𝑧 ∩ 𝐶 ) = ∅ → 𝑧 = 𝐷 ) ) → 𝐷 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfttc4lem1.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }
2		dfttc4lem1.2	⊢ 𝐶 ∈ V
3		dfttc4lem1.3	⊢ 𝐷 ∈ V
4		ineq2	⊢ ( 𝑦 = 𝐶 → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ 𝐶 ) )
5	4	neeq1d	⊢ ( 𝑦 = 𝐶 → ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ↔ ( 𝐴 ∩ 𝐶 ) ≠ ∅ ) )
6		ineq2	⊢ ( 𝑦 = 𝐶 → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ 𝐶 ) )
7	6	eqeq1d	⊢ ( 𝑦 = 𝐶 → ( ( 𝑧 ∩ 𝑦 ) = ∅ ↔ ( 𝑧 ∩ 𝐶 ) = ∅ ) )
8	7	imbi1d	⊢ ( 𝑦 = 𝐶 → ( ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ↔ ( ( 𝑧 ∩ 𝐶 ) = ∅ → 𝑧 = 𝐷 ) ) )
9	8	raleqbi1dv	⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ↔ ∀ 𝑧 ∈ 𝐶 ( ( 𝑧 ∩ 𝐶 ) = ∅ → 𝑧 = 𝐷 ) ) )
10	5 9	anbi12d	⊢ ( 𝑦 = 𝐶 → ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) ↔ ( ( 𝐴 ∩ 𝐶 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐶 ( ( 𝑧 ∩ 𝐶 ) = ∅ → 𝑧 = 𝐷 ) ) ) )
11	2 10	spcev	⊢ ( ( ( 𝐴 ∩ 𝐶 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐶 ( ( 𝑧 ∩ 𝐶 ) = ∅ → 𝑧 = 𝐷 ) ) → ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) )
12		eqeq2	⊢ ( 𝑥 = 𝐷 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝐷 ) )
13	12	imbi2d	⊢ ( 𝑥 = 𝐷 → ( ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ↔ ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) )
14	13	ralbidv	⊢ ( 𝑥 = 𝐷 → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) )
15	14	anbi2d	⊢ ( 𝑥 = 𝐷 → ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) ↔ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) ) )
16	15	exbidv	⊢ ( 𝑥 = 𝐷 → ( ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) ↔ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) ) )
17	3 16 1	elab2	⊢ ( 𝐷 ∈ 𝐵 ↔ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝐷 ) ) )
18	11 17	sylibr	⊢ ( ( ( 𝐴 ∩ 𝐶 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐶 ( ( 𝑧 ∩ 𝐶 ) = ∅ → 𝑧 = 𝐷 ) ) → 𝐷 ∈ 𝐵 )