Step |
Hyp |
Ref |
Expression |
1 |
|
elfvdm |
|- ( A e. ( R1 ` B ) -> B e. dom R1 ) |
2 |
|
r1val1 |
|- ( B e. dom R1 -> ( R1 ` B ) = U_ x e. B ~P ( R1 ` x ) ) |
3 |
2
|
eleq2d |
|- ( B e. dom R1 -> ( A e. ( R1 ` B ) <-> A e. U_ x e. B ~P ( R1 ` x ) ) ) |
4 |
|
eliun |
|- ( A e. U_ x e. B ~P ( R1 ` x ) <-> E. x e. B A e. ~P ( R1 ` x ) ) |
5 |
3 4
|
bitrdi |
|- ( B e. dom R1 -> ( A e. ( R1 ` B ) <-> E. x e. B A e. ~P ( R1 ` x ) ) ) |
6 |
|
r1funlim |
|- ( Fun R1 /\ Lim dom R1 ) |
7 |
6
|
simpri |
|- Lim dom R1 |
8 |
|
limord |
|- ( Lim dom R1 -> Ord dom R1 ) |
9 |
7 8
|
ax-mp |
|- Ord dom R1 |
10 |
|
ordtr1 |
|- ( Ord dom R1 -> ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 ) ) |
11 |
9 10
|
ax-mp |
|- ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 ) |
12 |
11
|
ancoms |
|- ( ( B e. dom R1 /\ x e. B ) -> x e. dom R1 ) |
13 |
|
r1sucg |
|- ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) ) |
14 |
13
|
eleq2d |
|- ( x e. dom R1 -> ( A e. ( R1 ` suc x ) <-> A e. ~P ( R1 ` x ) ) ) |
15 |
12 14
|
syl |
|- ( ( B e. dom R1 /\ x e. B ) -> ( A e. ( R1 ` suc x ) <-> A e. ~P ( R1 ` x ) ) ) |
16 |
|
ordsson |
|- ( Ord dom R1 -> dom R1 C_ On ) |
17 |
9 16
|
ax-mp |
|- dom R1 C_ On |
18 |
17 12
|
sselid |
|- ( ( B e. dom R1 /\ x e. B ) -> x e. On ) |
19 |
|
rabid |
|- ( x e. { x e. On | A e. ( R1 ` suc x ) } <-> ( x e. On /\ A e. ( R1 ` suc x ) ) ) |
20 |
|
intss1 |
|- ( x e. { x e. On | A e. ( R1 ` suc x ) } -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) |
21 |
19 20
|
sylbir |
|- ( ( x e. On /\ A e. ( R1 ` suc x ) ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) |
22 |
18 21
|
sylan |
|- ( ( ( B e. dom R1 /\ x e. B ) /\ A e. ( R1 ` suc x ) ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) |
23 |
22
|
ex |
|- ( ( B e. dom R1 /\ x e. B ) -> ( A e. ( R1 ` suc x ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) ) |
24 |
15 23
|
sylbird |
|- ( ( B e. dom R1 /\ x e. B ) -> ( A e. ~P ( R1 ` x ) -> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) ) |
25 |
24
|
reximdva |
|- ( B e. dom R1 -> ( E. x e. B A e. ~P ( R1 ` x ) -> E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) ) |
26 |
5 25
|
sylbid |
|- ( B e. dom R1 -> ( A e. ( R1 ` B ) -> E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) ) |
27 |
1 26
|
mpcom |
|- ( A e. ( R1 ` B ) -> E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) |
28 |
|
r1elwf |
|- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) ) |
29 |
|
rankvalb |
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } ) |
30 |
28 29
|
syl |
|- ( A e. ( R1 ` B ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } ) |
31 |
30
|
sseq1d |
|- ( A e. ( R1 ` B ) -> ( ( rank ` A ) C_ x <-> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) ) |
32 |
31
|
adantr |
|- ( ( A e. ( R1 ` B ) /\ x e. B ) -> ( ( rank ` A ) C_ x <-> |^| { x e. On | A e. ( R1 ` suc x ) } C_ x ) ) |
33 |
|
rankon |
|- ( rank ` A ) e. On |
34 |
17 1
|
sselid |
|- ( A e. ( R1 ` B ) -> B e. On ) |
35 |
|
ontr2 |
|- ( ( ( rank ` A ) e. On /\ B e. On ) -> ( ( ( rank ` A ) C_ x /\ x e. B ) -> ( rank ` A ) e. B ) ) |
36 |
33 34 35
|
sylancr |
|- ( A e. ( R1 ` B ) -> ( ( ( rank ` A ) C_ x /\ x e. B ) -> ( rank ` A ) e. B ) ) |
37 |
36
|
expcomd |
|- ( A e. ( R1 ` B ) -> ( x e. B -> ( ( rank ` A ) C_ x -> ( rank ` A ) e. B ) ) ) |
38 |
37
|
imp |
|- ( ( A e. ( R1 ` B ) /\ x e. B ) -> ( ( rank ` A ) C_ x -> ( rank ` A ) e. B ) ) |
39 |
32 38
|
sylbird |
|- ( ( A e. ( R1 ` B ) /\ x e. B ) -> ( |^| { x e. On | A e. ( R1 ` suc x ) } C_ x -> ( rank ` A ) e. B ) ) |
40 |
39
|
rexlimdva |
|- ( A e. ( R1 ` B ) -> ( E. x e. B |^| { x e. On | A e. ( R1 ` suc x ) } C_ x -> ( rank ` A ) e. B ) ) |
41 |
27 40
|
mpd |
|- ( A e. ( R1 ` B ) -> ( rank ` A ) e. B ) |