functhinclem2

	Ref	Expression
Hypotheses	functhinclem2.x	$⊢ φ \to X \in B$
	functhinclem2.y	$⊢ φ \to Y \in B$
	functhinclem2.1	$⊢ φ \to \forall x \in B \forall y \in B (F (x) J F (y) = \emptyset \to x H y = \emptyset)$
Assertion	functhinclem2	$⊢ φ \to (F (X) J F (Y) = \emptyset \to X H Y = \emptyset)$

Step	Hyp	Ref	Expression
1		functhinclem2.x	$⊢ φ \to X \in B$
2		functhinclem2.y	$⊢ φ \to Y \in B$
3		functhinclem2.1	$⊢ φ \to \forall x \in B \forall y \in B (F (x) J F (y) = \emptyset \to x H y = \emptyset)$
4		simpl	$⊢ (x = X \land y = Y) \to x = X$
5	4	fveq2d	$⊢ (x = X \land y = Y) \to F (x) = F (X)$
6		simpr	$⊢ (x = X \land y = Y) \to y = Y$
7	6	fveq2d	$⊢ (x = X \land y = Y) \to F (y) = F (Y)$
8	5 7	oveq12d	$⊢ (x = X \land y = Y) \to F (x) J F (y) = F (X) J F (Y)$
9	8	eqeq1d	$⊢ (x = X \land y = Y) \to (F (x) J F (y) = \emptyset \leftrightarrow F (X) J F (Y) = \emptyset)$
10		oveq12	$⊢ (x = X \land y = Y) \to x H y = X H Y$
11	10	eqeq1d	$⊢ (x = X \land y = Y) \to (x H y = \emptyset \leftrightarrow X H Y = \emptyset)$
12	9 11	imbi12d	$⊢ (x = X \land y = Y) \to ((F (x) J F (y) = \emptyset \to x H y = \emptyset) \leftrightarrow (F (X) J F (Y) = \emptyset \to X H Y = \emptyset))$
13	12	rspc2gv	$⊢ (X \in B \land Y \in B) \to (\forall x \in B \forall y \in B (F (x) J F (y) = \emptyset \to x H y = \emptyset) \to (F (X) J F (Y) = \emptyset \to X H Y = \emptyset))$
14	13	imp	$⊢ ((X \in B \land Y \in B) \land \forall x \in B \forall y \in B (F (x) J F (y) = \emptyset \to x H y = \emptyset)) \to (F (X) J F (Y) = \emptyset \to X H Y = \emptyset)$
15	1 2 3 14	syl21anc	$⊢ φ \to (F (X) J F (Y) = \emptyset \to X H Y = \emptyset)$

Metamath Proof Explorer