Metamath Proof Explorer

Theorem php2OLD

Description: Obsolete version of php2 as of 20-Nov-2024. (Contributed by NM, 31-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	php2OLD	$⊢ (A \in ω \land B \subset A) \to B ≺ A$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = A \to (x \in ω \leftrightarrow A \in ω)$
2		psseq2	$⊢ x = A \to (B \subset x \leftrightarrow B \subset A)$
3	1 2	anbi12d	$⊢ x = A \to ((x \in ω \land B \subset x) \leftrightarrow (A \in ω \land B \subset A))$
4		breq2	$⊢ x = A \to (B ≺ x \leftrightarrow B ≺ A)$
5	3 4	imbi12d	$⊢ x = A \to (((x \in ω \land B \subset x) \to B ≺ x) \leftrightarrow ((A \in ω \land B \subset A) \to B ≺ A))$
6		vex	$⊢ x \in V$
7		pssss	$⊢ B \subset x \to B \subseteq x$
8		ssdomg	$⊢ x \in V \to (B \subseteq x \to B ≼ x)$
9	6 7 8	mpsyl	$⊢ B \subset x \to B ≼ x$
10	9	adantl	$⊢ (x \in ω \land B \subset x) \to B ≼ x$
11		php	$⊢ (x \in ω \land B \subset x) \to \neg x \approx B$
12		ensym	$⊢ B \approx x \to x \approx B$
13	11 12	nsyl	$⊢ (x \in ω \land B \subset x) \to \neg B \approx x$
14		brsdom	$⊢ B ≺ x \leftrightarrow (B ≼ x \land \neg B \approx x)$
15	10 13 14	sylanbrc	$⊢ (x \in ω \land B \subset x) \to B ≺ x$
16	5 15	vtoclg	$⊢ A \in ω \to ((A \in ω \land B \subset A) \to B ≺ A)$
17	16	anabsi5	$⊢ (A \in ω \land B \subset A) \to B ≺ A$