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 φ ψ
omsinds.2 x = A φ χ
omsinds.3 x ω y x ψ φ
Assertion omsindsOLD A ω χ

Proof

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