Metamath Proof Explorer


Theorem aomclem7

Description: Lemma for dfac11 . ( R1A ) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem6.b B=ab|cR1domzcb¬cadR1domzdzdomzcdadb
aomclem6.c C=aVsupyaR1domzB
aomclem6.d D=recsaVCR1domzrana
aomclem6.e E=ab|D-1aD-1b
aomclem6.f F=ab|rankaErankbranka=rankbazsucrankab
aomclem6.g G=ifdomz=domzFER1domz×R1domz
aomclem6.h H=recszVG
aomclem6.a φAOn
aomclem6.y φa𝒫R1Aaya𝒫aFin
Assertion aomclem7 φbbWeR1A

Proof

Step Hyp Ref Expression
1 aomclem6.b B=ab|cR1domzcb¬cadR1domzdzdomzcdadb
2 aomclem6.c C=aVsupyaR1domzB
3 aomclem6.d D=recsaVCR1domzrana
4 aomclem6.e E=ab|D-1aD-1b
5 aomclem6.f F=ab|rankaErankbranka=rankbazsucrankab
6 aomclem6.g G=ifdomz=domzFER1domz×R1domz
7 aomclem6.h H=recszVG
8 aomclem6.a φAOn
9 aomclem6.y φa𝒫R1Aaya𝒫aFin
10 1 2 3 4 5 6 7 8 9 aomclem6 φHAWeR1A
11 fvex HAV
12 weeq1 b=HAbWeR1AHAWeR1A
13 11 12 spcev HAWeR1AbbWeR1A
14 10 13 syl φbbWeR1A