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 | |
|
aomclem2.c | |
||
aomclem2.on | |
||
aomclem2.su | |
||
aomclem2.we | |
||
aomclem2.a | |
||
aomclem2.za | |
||
aomclem2.y | |
||
Assertion | aomclem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aomclem2.b | |
|
2 | aomclem2.c | |
|
3 | aomclem2.on | |
|
4 | aomclem2.su | |
|
5 | aomclem2.we | |
|
6 | aomclem2.a | |
|
7 | aomclem2.za | |
|
8 | aomclem2.y | |
|
9 | vex | |
|
10 | 3 6 | jca | |
11 | r1ord3 | |
|
12 | 10 7 11 | sylc | |
13 | 12 | sspwd | |
14 | 13 | sseld | |
15 | rsp | |
|
16 | 8 14 15 | sylsyld | |
17 | 16 | 3imp | |
18 | 17 | eldifad | |
19 | inss1 | |
|
20 | 19 | sseli | |
21 | 20 | elpwid | |
22 | 18 21 | syl | |
23 | 1 3 4 5 | aomclem1 | |
24 | 23 | 3ad2ant1 | |
25 | inss2 | |
|
26 | 25 18 | sselid | |
27 | eldifsni | |
|
28 | 17 27 | syl | |
29 | elpwi | |
|
30 | 29 | 3ad2ant2 | |
31 | 22 30 | sstrd | |
32 | fisupcl | |
|
33 | 24 26 28 31 32 | syl13anc | |
34 | 22 33 | sseldd | |
35 | 2 | fvmpt2 | |
36 | 9 34 35 | sylancr | |
37 | 36 34 | eqeltrd | |
38 | 37 | 3exp | |
39 | 38 | ralrimiv | |