prsrcmpltd

Description: If a statement is true for all pairs of elements of a class, all pairs of elements of its complement relative to a second class, and all pairs with one element in each, then it is true for all pairs of elements of the second class. (Contributed by BTernaryTau, 27-Sep-2023)

	Ref	Expression
Hypotheses	prsrcmpltd.1	$⊢ φ \to ((C \in A \land D \in A) \to ψ)$
	prsrcmpltd.2	$⊢ φ \to ((C \in A \land D \in (B ∖ A)) \to ψ)$
	prsrcmpltd.3	$⊢ φ \to ((C \in (B ∖ A) \land D \in A) \to ψ)$
	prsrcmpltd.4	$⊢ φ \to ((C \in (B ∖ A) \land D \in (B ∖ A)) \to ψ)$
Assertion	prsrcmpltd	$⊢ φ \to ((C \in B \land D \in B) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		prsrcmpltd.1	$⊢ φ \to ((C \in A \land D \in A) \to ψ)$
2		prsrcmpltd.2	$⊢ φ \to ((C \in A \land D \in (B ∖ A)) \to ψ)$
3		prsrcmpltd.3	$⊢ φ \to ((C \in (B ∖ A) \land D \in A) \to ψ)$
4		prsrcmpltd.4	$⊢ φ \to ((C \in (B ∖ A) \land D \in (B ∖ A)) \to ψ)$
5	1	expdimp	$⊢ (φ \land C \in A) \to (D \in A \to ψ)$
6	2	expdimp	$⊢ (φ \land C \in A) \to (D \in (B ∖ A) \to ψ)$
7	5 6	srcmpltd	$⊢ (φ \land C \in A) \to (D \in B \to ψ)$
8	7	impancom	$⊢ (φ \land D \in B) \to (C \in A \to ψ)$
9	3	expdimp	$⊢ (φ \land C \in (B ∖ A)) \to (D \in A \to ψ)$
10	4	expdimp	$⊢ (φ \land C \in (B ∖ A)) \to (D \in (B ∖ A) \to ψ)$
11	9 10	srcmpltd	$⊢ (φ \land C \in (B ∖ A)) \to (D \in B \to ψ)$
12	11	impancom	$⊢ (φ \land D \in B) \to (C \in (B ∖ A) \to ψ)$
13	8 12	srcmpltd	$⊢ (φ \land D \in B) \to (C \in B \to ψ)$
14	13	ex	$⊢ φ \to (D \in B \to (C \in B \to ψ))$
15	14	impcomd	$⊢ φ \to ((C \in B \land D \in B) \to ψ)$

Metamath Proof Explorer

Theorem prsrcmpltd

Proof