Metamath Proof Explorer


Theorem onfrALTlem3

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem3 aOnaxa¬ax=yaxaxy=

Proof

Step Hyp Ref Expression
1 ssid axax
2 simpr xa¬ax=¬ax=
3 2 a1i aOnaxa¬ax=¬ax=
4 df-ne ax¬ax=
5 3 4 syl6ibr aOnaxa¬ax=ax
6 pm3.2 axaxaxaxaxax
7 1 5 6 mpsylsyld aOnaxa¬ax=axaxax
8 vex xV
9 8 inex2 axV
10 inss2 axx
11 simpl aOnaaOn
12 simpl xa¬ax=xa
13 ssel aOnxaxOn
14 11 12 13 syl2im aOnaxa¬ax=xOn
15 eloni xOnOrdx
16 14 15 syl6 aOnaxa¬ax=Ordx
17 ordwe OrdxEWex
18 16 17 syl6 aOnaxa¬ax=EWex
19 wess axxEWexEWeax
20 10 18 19 mpsylsyld aOnaxa¬ax=EWeax
21 wefr EWeaxEFrax
22 20 21 syl6 aOnaxa¬ax=EFrax
23 dfepfr EFraxbbaxbybby=
24 22 23 imbitrdi aOnaxa¬ax=bbaxbybby=
25 spsbc axVbbaxbybby=[˙ax/b]˙baxbybby=
26 9 24 25 mpsylsyld aOnaxa¬ax=[˙ax/b]˙baxbybby=
27 onfrALTlem5 [˙ax/b]˙baxbybby=axaxaxyaxaxy=
28 26 27 imbitrdi aOnaxa¬ax=axaxaxyaxaxy=
29 7 28 mpdd aOnaxa¬ax=yaxaxy=