Metamath Proof Explorer


Theorem aomclem2

Description: Lemma for dfac11 . Successor case 2, a choice function for subsets of ( R1dom z ) . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses aomclem2.b B=ab|cR1domzcb¬cadR1domzdzdomzcdadb
aomclem2.c C=aVsupyaR1domzB
aomclem2.on φdomzOn
aomclem2.su φdomz=sucdomz
aomclem2.we φadomzzaWeR1a
aomclem2.a φAOn
aomclem2.za φdomzA
aomclem2.y φa𝒫R1Aaya𝒫aFin
Assertion aomclem2 φa𝒫R1domzaCaa

Proof

Step Hyp Ref Expression
1 aomclem2.b B=ab|cR1domzcb¬cadR1domzdzdomzcdadb
2 aomclem2.c C=aVsupyaR1domzB
3 aomclem2.on φdomzOn
4 aomclem2.su φdomz=sucdomz
5 aomclem2.we φadomzzaWeR1a
6 aomclem2.a φAOn
7 aomclem2.za φdomzA
8 aomclem2.y φa𝒫R1Aaya𝒫aFin
9 vex aV
10 3 6 jca φdomzOnAOn
11 r1ord3 domzOnAOndomzAR1domzR1A
12 10 7 11 sylc φR1domzR1A
13 12 sspwd φ𝒫R1domz𝒫R1A
14 13 sseld φa𝒫R1domza𝒫R1A
15 rsp a𝒫R1Aaya𝒫aFina𝒫R1Aaya𝒫aFin
16 8 14 15 sylsyld φa𝒫R1domzaya𝒫aFin
17 16 3imp φa𝒫R1domzaya𝒫aFin
18 17 eldifad φa𝒫R1domzaya𝒫aFin
19 inss1 𝒫aFin𝒫a
20 19 sseli ya𝒫aFinya𝒫a
21 20 elpwid ya𝒫aFinyaa
22 18 21 syl φa𝒫R1domzayaa
23 1 3 4 5 aomclem1 φBOrR1domz
24 23 3ad2ant1 φa𝒫R1domzaBOrR1domz
25 inss2 𝒫aFinFin
26 25 18 sselid φa𝒫R1domzayaFin
27 eldifsni ya𝒫aFinya
28 17 27 syl φa𝒫R1domzaya
29 elpwi a𝒫R1domzaR1domz
30 29 3ad2ant2 φa𝒫R1domzaaR1domz
31 22 30 sstrd φa𝒫R1domzayaR1domz
32 fisupcl BOrR1domzyaFinyayaR1domzsupyaR1domzBya
33 24 26 28 31 32 syl13anc φa𝒫R1domzasupyaR1domzBya
34 22 33 sseldd φa𝒫R1domzasupyaR1domzBa
35 2 fvmpt2 aVsupyaR1domzBaCa=supyaR1domzB
36 9 34 35 sylancr φa𝒫R1domzaCa=supyaR1domzB
37 36 34 eqeltrd φa𝒫R1domzaCaa
38 37 3exp φa𝒫R1domzaCaa
39 38 ralrimiv φa𝒫R1domzaCaa