Metamath Proof Explorer

Theorem dfttc4lem1

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

		Ref	Expression
	Hypotheses	dfttc4lem1.1	$⊢ B = \{x \| \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x))\}$
		dfttc4lem1.2	$⊢ C \in V$
		dfttc4lem1.3	$⊢ D \in V$
	Assertion	dfttc4lem1	$⊢ (A \cap C \neq \emptyset \land \forall z \in C (z \cap C = \emptyset \to z = D)) \to D \in B$

Proof

Step	Hyp	Ref	Expression
1		dfttc4lem1.1	$⊢ B = \{x \| \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x))\}$
2		dfttc4lem1.2	$⊢ C \in V$
3		dfttc4lem1.3	$⊢ D \in V$
4		ineq2	$⊢ y = C \to A \cap y = A \cap C$
5	4	neeq1d	$⊢ y = C \to (A \cap y \neq \emptyset \leftrightarrow A \cap C \neq \emptyset)$
6		ineq2	$⊢ y = C \to z \cap y = z \cap C$
7	6	eqeq1d	$⊢ y = C \to (z \cap y = \emptyset \leftrightarrow z \cap C = \emptyset)$
8	7	imbi1d	$⊢ y = C \to ((z \cap y = \emptyset \to z = D) \leftrightarrow (z \cap C = \emptyset \to z = D))$
9	8	raleqbi1dv	$⊢ y = C \to (\forall z \in y (z \cap y = \emptyset \to z = D) \leftrightarrow \forall z \in C (z \cap C = \emptyset \to z = D))$
10	5 9	anbi12d	$⊢ y = C \to ((A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = D)) \leftrightarrow (A \cap C \neq \emptyset \land \forall z \in C (z \cap C = \emptyset \to z = D)))$
11	2 10	spcev	$⊢ (A \cap C \neq \emptyset \land \forall z \in C (z \cap C = \emptyset \to z = D)) \to \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = D))$
12		eqeq2	$⊢ x = D \to (z = x \leftrightarrow z = D)$
13	12	imbi2d	$⊢ x = D \to ((z \cap y = \emptyset \to z = x) \leftrightarrow (z \cap y = \emptyset \to z = D))$
14	13	ralbidv	$⊢ x = D \to (\forall z \in y (z \cap y = \emptyset \to z = x) \leftrightarrow \forall z \in y (z \cap y = \emptyset \to z = D))$
15	14	anbi2d	$⊢ x = D \to ((A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x)) \leftrightarrow (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = D)))$
16	15	exbidv	$⊢ x = D \to (\exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x)) \leftrightarrow \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = D)))$
17	3 16 1	elab2	$⊢ D \in B \leftrightarrow \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = D))$
18	11 17	sylibr	$⊢ (A \cap C \neq \emptyset \land \forall z \in C (z \cap C = \emptyset \to z = D)) \to D \in B$