Metamath Proof Explorer

Theorem omsindsOLD

Description: Obsolete version of omsinds as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	omsinds.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
		omsinds.2	$⊢ x = A \to (φ \leftrightarrow χ)$
		omsinds.3	$⊢ x \in ω \to (\forall y \in x ψ \to φ)$
	Assertion	omsindsOLD	$⊢ A \in ω \to χ$

Proof

Step	Hyp	Ref	Expression
1		omsinds.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		omsinds.2	$⊢ x = A \to (φ \leftrightarrow χ)$
3		omsinds.3	$⊢ x \in ω \to (\forall y \in x ψ \to φ)$
4		omsson	$⊢ ω \subseteq On$
5		epweon	$⊢ E We On$
6		wess	$⊢ ω \subseteq On \to (E We On \to E We ω)$
7	4 5 6	mp2	$⊢ E We ω$
8		epse	$⊢ E Se ω$
9		predep	$⊢ x \in ω \to Pred (E, ω, x) = ω \cap x$
10		ordom	$⊢ Ord ω$
11		ordtr	$⊢ Ord ω \to Tr ω$
12		trss	$⊢ Tr ω \to (x \in ω \to x \subseteq ω)$
13	10 11 12	mp2b	$⊢ x \in ω \to x \subseteq ω$
14		sseqin2	$⊢ x \subseteq ω \leftrightarrow ω \cap x = x$
15	13 14	sylib	$⊢ x \in ω \to ω \cap x = x$
16	9 15	eqtrd	$⊢ x \in ω \to Pred (E, ω, x) = x$
17	16	raleqdv	$⊢ x \in ω \to (\forall y \in Pred (E, ω, x) ψ \leftrightarrow \forall y \in x ψ)$
18	17 3	sylbid	$⊢ x \in ω \to (\forall y \in Pred (E, ω, x) ψ \to φ)$
19	7 8 1 2 18	wfis3	$⊢ A \in ω \to χ$