Step |
Hyp |
Ref |
Expression |
1 |
|
inawina |
⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw ) |
2 |
|
winaon |
⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On ) |
3 |
1 2
|
syl |
⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ On ) |
4 |
|
winalim |
⊢ ( 𝐴 ∈ Inaccw → Lim 𝐴 ) |
5 |
1 4
|
syl |
⊢ ( 𝐴 ∈ Inacc → Lim 𝐴 ) |
6 |
|
r1lim |
⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ) |
7 |
3 5 6
|
syl2anc |
⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ) |
8 |
|
onelon |
⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On ) |
9 |
3 8
|
sylan |
⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On ) |
10 |
|
eleq1 |
⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) ) |
11 |
|
fveq2 |
⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) ) |
12 |
11
|
breq1d |
⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ↔ ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) ) |
13 |
10 12
|
imbi12d |
⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ↔ ( ∅ ∈ 𝐴 → ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) ) ) |
14 |
|
eleq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) |
15 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) ) |
16 |
15
|
breq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) |
17 |
14 16
|
imbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) |
18 |
|
eleq1 |
⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴 ) ) |
19 |
|
fveq2 |
⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) ) |
20 |
19
|
breq1d |
⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ↔ ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) |
21 |
18 20
|
imbi12d |
⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ↔ ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) ) |
22 |
|
ne0i |
⊢ ( ∅ ∈ 𝐴 → 𝐴 ≠ ∅ ) |
23 |
|
0sdomg |
⊢ ( 𝐴 ∈ On → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
24 |
22 23
|
syl5ibr |
⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ∅ ≺ 𝐴 ) ) |
25 |
|
r10 |
⊢ ( 𝑅1 ‘ ∅ ) = ∅ |
26 |
25
|
breq1i |
⊢ ( ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ↔ ∅ ≺ 𝐴 ) |
27 |
24 26
|
syl6ibr |
⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) ) |
28 |
1 2 27
|
3syl |
⊢ ( 𝐴 ∈ Inacc → ( ∅ ∈ 𝐴 → ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) ) |
29 |
|
eloni |
⊢ ( 𝐴 ∈ On → Ord 𝐴 ) |
30 |
|
ordtr |
⊢ ( Ord 𝐴 → Tr 𝐴 ) |
31 |
29 30
|
syl |
⊢ ( 𝐴 ∈ On → Tr 𝐴 ) |
32 |
|
trsuc |
⊢ ( ( Tr 𝐴 ∧ suc 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) |
33 |
32
|
ex |
⊢ ( Tr 𝐴 → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
34 |
3 31 33
|
3syl |
⊢ ( 𝐴 ∈ Inacc → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
35 |
34
|
adantl |
⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ Inacc ) → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
36 |
|
r1suc |
⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) ) |
37 |
|
fvex |
⊢ ( 𝑅1 ‘ 𝑦 ) ∈ V |
38 |
37
|
cardid |
⊢ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≈ ( 𝑅1 ‘ 𝑦 ) |
39 |
38
|
ensymi |
⊢ ( 𝑅1 ‘ 𝑦 ) ≈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) |
40 |
|
pwen |
⊢ ( ( 𝑅1 ‘ 𝑦 ) ≈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝒫 ( 𝑅1 ‘ 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
41 |
39 40
|
ax-mp |
⊢ 𝒫 ( 𝑅1 ‘ 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) |
42 |
36 41
|
eqbrtrdi |
⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
43 |
|
winacard |
⊢ ( 𝐴 ∈ Inaccw → ( card ‘ 𝐴 ) = 𝐴 ) |
44 |
43
|
eleq2d |
⊢ ( 𝐴 ∈ Inaccw → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) ) |
45 |
|
cardsdom |
⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ∈ V ∧ 𝐴 ∈ On ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) |
46 |
37 2 45
|
sylancr |
⊢ ( 𝐴 ∈ Inaccw → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) |
47 |
44 46
|
bitr3d |
⊢ ( 𝐴 ∈ Inaccw → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) |
48 |
1 47
|
syl |
⊢ ( 𝐴 ∈ Inacc → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) |
49 |
|
elina |
⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 ) ) |
50 |
49
|
simp3bi |
⊢ ( 𝐴 ∈ Inacc → ∀ 𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 ) |
51 |
|
pweq |
⊢ ( 𝑧 = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝒫 𝑧 = 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
52 |
51
|
breq1d |
⊢ ( 𝑧 = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) ) |
53 |
52
|
rspccv |
⊢ ( ∀ 𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) ) |
54 |
50 53
|
syl |
⊢ ( 𝐴 ∈ Inacc → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) ) |
55 |
48 54
|
sylbird |
⊢ ( 𝐴 ∈ Inacc → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) ) |
56 |
55
|
imp |
⊢ ( ( 𝐴 ∈ Inacc ∧ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) |
57 |
|
ensdomtr |
⊢ ( ( ( 𝑅1 ‘ suc 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) |
58 |
42 56 57
|
syl2an |
⊢ ( ( 𝑦 ∈ On ∧ ( 𝐴 ∈ Inacc ∧ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) |
59 |
58
|
expr |
⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ Inacc ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) |
60 |
35 59
|
imim12d |
⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ Inacc ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) ) |
61 |
60
|
ex |
⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ Inacc → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) ) ) |
62 |
|
vex |
⊢ 𝑥 ∈ V |
63 |
|
r1lim |
⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ) |
64 |
62 63
|
mpan |
⊢ ( Lim 𝑥 → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ) |
65 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑧 |
66 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 𝑅1 ‘ 𝑧 ) |
67 |
|
nfcv |
⊢ Ⅎ 𝑦 ≼ |
68 |
|
nfiu1 |
⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) |
69 |
66 67 68
|
nfbr |
⊢ Ⅎ 𝑦 ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) |
70 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( 𝑅1 ‘ 𝑦 ) = ( 𝑅1 ‘ 𝑧 ) ) |
71 |
70
|
breq1d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝑅1 ‘ 𝑦 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ↔ ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
72 |
|
fvex |
⊢ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ V |
73 |
62 72
|
iunex |
⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ V |
74 |
|
ssiun2 |
⊢ ( 𝑦 ∈ 𝑥 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
75 |
|
ssdomg |
⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ V → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
76 |
73 74 75
|
mpsyl |
⊢ ( 𝑦 ∈ 𝑥 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
77 |
|
endomtr |
⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ≈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑅1 ‘ 𝑦 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
78 |
39 76 77
|
sylancr |
⊢ ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
79 |
65 69 71 78
|
vtoclgaf |
⊢ ( 𝑧 ∈ 𝑥 → ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
80 |
79
|
rgen |
⊢ ∀ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) |
81 |
|
iundom |
⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
82 |
62 80 81
|
mp2an |
⊢ ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
83 |
62 73
|
unex |
⊢ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V |
84 |
|
ssun2 |
⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
85 |
|
ssdomg |
⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V → ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
86 |
83 84 85
|
mp2 |
⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
87 |
62
|
xpdom2 |
⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
88 |
86 87
|
ax-mp |
⊢ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
89 |
|
ssun1 |
⊢ 𝑥 ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
90 |
|
ssdomg |
⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V → ( 𝑥 ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → 𝑥 ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
91 |
83 89 90
|
mp2 |
⊢ 𝑥 ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
92 |
83
|
xpdom1 |
⊢ ( 𝑥 ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
93 |
91 92
|
ax-mp |
⊢ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
94 |
|
domtr |
⊢ ( ( ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ∧ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
95 |
88 93 94
|
mp2an |
⊢ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
96 |
|
limomss |
⊢ ( Lim 𝑥 → ω ⊆ 𝑥 ) |
97 |
96 89
|
sstrdi |
⊢ ( Lim 𝑥 → ω ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
98 |
|
ssdomg |
⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V → ( ω ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ω ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
99 |
83 97 98
|
mpsyl |
⊢ ( Lim 𝑥 → ω ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
100 |
|
infxpidm |
⊢ ( ω ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≈ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
101 |
99 100
|
syl |
⊢ ( Lim 𝑥 → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≈ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
102 |
|
domentr |
⊢ ( ( ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ∧ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≈ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
103 |
95 101 102
|
sylancr |
⊢ ( Lim 𝑥 → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
104 |
|
domtr |
⊢ ( ( ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∧ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) → ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
105 |
82 103 104
|
sylancr |
⊢ ( Lim 𝑥 → ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
106 |
64 105
|
eqbrtrd |
⊢ ( Lim 𝑥 → ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
107 |
106
|
ad2antlr |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
108 |
|
eleq1a |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 = 𝑥 → 𝐴 ∈ 𝐴 ) ) |
109 |
|
ordirr |
⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 ) |
110 |
3 29 109
|
3syl |
⊢ ( 𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴 ) |
111 |
108 110
|
nsyli |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥 ) ) |
112 |
111
|
imp |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc ) → ¬ 𝐴 = 𝑥 ) |
113 |
112
|
ad2ant2r |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ¬ 𝐴 = 𝑥 ) |
114 |
|
simpll |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝑥 ∈ 𝐴 ) |
115 |
|
limord |
⊢ ( Lim 𝑥 → Ord 𝑥 ) |
116 |
62
|
elon |
⊢ ( 𝑥 ∈ On ↔ Ord 𝑥 ) |
117 |
115 116
|
sylibr |
⊢ ( Lim 𝑥 → 𝑥 ∈ On ) |
118 |
117
|
ad2antlr |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝑥 ∈ On ) |
119 |
|
cardf |
⊢ card : V ⟶ On |
120 |
|
r1fnon |
⊢ 𝑅1 Fn On |
121 |
|
dffn2 |
⊢ ( 𝑅1 Fn On ↔ 𝑅1 : On ⟶ V ) |
122 |
120 121
|
mpbi |
⊢ 𝑅1 : On ⟶ V |
123 |
|
fco |
⊢ ( ( card : V ⟶ On ∧ 𝑅1 : On ⟶ V ) → ( card ∘ 𝑅1 ) : On ⟶ On ) |
124 |
119 122 123
|
mp2an |
⊢ ( card ∘ 𝑅1 ) : On ⟶ On |
125 |
|
onss |
⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On ) |
126 |
|
fssres |
⊢ ( ( ( card ∘ 𝑅1 ) : On ⟶ On ∧ 𝑥 ⊆ On ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ On ) |
127 |
124 125 126
|
sylancr |
⊢ ( 𝑥 ∈ On → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ On ) |
128 |
|
ffn |
⊢ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ On → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) Fn 𝑥 ) |
129 |
118 127 128
|
3syl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) Fn 𝑥 ) |
130 |
3
|
ad2antlr |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝐴 ∈ On ) |
131 |
|
simpr |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 ) |
132 |
|
simplll |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝐴 ) |
133 |
|
ontr1 |
⊢ ( 𝐴 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) ) |
134 |
133
|
imp |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 ) |
135 |
130 131 132 134
|
syl12anc |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 ) |
136 |
37 130 45
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) |
137 |
1 43
|
syl |
⊢ ( 𝐴 ∈ Inacc → ( card ‘ 𝐴 ) = 𝐴 ) |
138 |
137
|
ad2antlr |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 ) |
139 |
138
|
eleq2d |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) ) |
140 |
136 139
|
bitr3d |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) ) |
141 |
140
|
biimpd |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) ) |
142 |
135 141
|
embantd |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) ) |
143 |
117
|
ad2antlr |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) → 𝑥 ∈ On ) |
144 |
|
fvres |
⊢ ( 𝑦 ∈ 𝑥 → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ) |
145 |
144
|
adantl |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ) |
146 |
|
onelon |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On ) |
147 |
|
fvco3 |
⊢ ( ( 𝑅1 : On ⟶ V ∧ 𝑦 ∈ On ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
148 |
122 146 147
|
sylancr |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
149 |
145 148
|
eqtrd |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
150 |
143 149
|
sylan |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
151 |
150
|
eleq1d |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) ) |
152 |
142 151
|
sylibrd |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) ) |
153 |
152
|
ralimdva |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) ) |
154 |
153
|
impr |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) |
155 |
|
ffnfv |
⊢ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ↔ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) ) |
156 |
129 154 155
|
sylanbrc |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ) |
157 |
|
eleq2 |
⊢ ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
158 |
157
|
biimpa |
⊢ ( ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
159 |
|
eliun |
⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ 𝑥 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
160 |
|
cardon |
⊢ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On |
161 |
160
|
onelssi |
⊢ ( 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝑧 ⊆ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
162 |
149
|
sseq2d |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ↔ 𝑧 ⊆ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
163 |
161 162
|
syl5ibr |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
164 |
163
|
reximdva |
⊢ ( 𝑥 ∈ On → ( ∃ 𝑦 ∈ 𝑥 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
165 |
159 164
|
syl5bi |
⊢ ( 𝑥 ∈ On → ( 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
166 |
158 165
|
syl5 |
⊢ ( 𝑥 ∈ On → ( ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
167 |
166
|
expdimp |
⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
168 |
167
|
ralrimiv |
⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) |
169 |
168
|
ex |
⊢ ( 𝑥 ∈ On → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
170 |
118 169
|
syl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
171 |
|
ffun |
⊢ ( ( card ∘ 𝑅1 ) : On ⟶ On → Fun ( card ∘ 𝑅1 ) ) |
172 |
124 171
|
ax-mp |
⊢ Fun ( card ∘ 𝑅1 ) |
173 |
|
resfunexg |
⊢ ( ( Fun ( card ∘ 𝑅1 ) ∧ 𝑥 ∈ V ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ∈ V ) |
174 |
172 62 173
|
mp2an |
⊢ ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ∈ V |
175 |
|
feq1 |
⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( 𝑤 : 𝑥 ⟶ 𝐴 ↔ ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ) ) |
176 |
|
fveq1 |
⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( 𝑤 ‘ 𝑦 ) = ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) |
177 |
176
|
sseq2d |
⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ↔ 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
178 |
177
|
rexbidv |
⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
179 |
178
|
ralbidv |
⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) |
180 |
175 179
|
anbi12d |
⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) ↔ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) ) |
181 |
174 180
|
spcev |
⊢ ( ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) → ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) ) |
182 |
156 170 181
|
syl6an |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) ) ) |
183 |
3
|
ad2antrl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝐴 ∈ On ) |
184 |
|
cfflb |
⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) ) |
185 |
183 118 184
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) ) |
186 |
182 185
|
syld |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) ) |
187 |
49
|
simp2bi |
⊢ ( 𝐴 ∈ Inacc → ( cf ‘ 𝐴 ) = 𝐴 ) |
188 |
187
|
sseq1d |
⊢ ( 𝐴 ∈ Inacc → ( ( cf ‘ 𝐴 ) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) ) |
189 |
188
|
ad2antrl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( cf ‘ 𝐴 ) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) ) |
190 |
186 189
|
sylibd |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝐴 ⊆ 𝑥 ) ) |
191 |
|
ontri1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴 ) ) |
192 |
183 118 191
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴 ) ) |
193 |
190 192
|
sylibd |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ¬ 𝑥 ∈ 𝐴 ) ) |
194 |
114 193
|
mt2d |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ¬ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
195 |
|
iunon |
⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) |
196 |
62 195
|
mpan |
⊢ ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) |
197 |
160
|
a1i |
⊢ ( 𝑦 ∈ 𝑥 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) |
198 |
196 197
|
mprg |
⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On |
199 |
|
eqcom |
⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ↔ 𝐴 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
200 |
|
eloni |
⊢ ( 𝑥 ∈ On → Ord 𝑥 ) |
201 |
|
eloni |
⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
202 |
|
ordequn |
⊢ ( ( Ord 𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝐴 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
203 |
200 201 202
|
syl2an |
⊢ ( ( 𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ( 𝐴 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
204 |
199 203
|
syl5bi |
⊢ ( ( 𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
205 |
118 198 204
|
sylancl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) |
206 |
113 194 205
|
mtord |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ¬ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) |
207 |
|
onelss |
⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) ) |
208 |
183 114 207
|
sylc |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝑥 ⊆ 𝐴 ) |
209 |
|
onelss |
⊢ ( 𝐴 ∈ On → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) ) |
210 |
130 142 209
|
sylsyld |
⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) ) |
211 |
210
|
ralimdva |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) ) |
212 |
211
|
impr |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) |
213 |
|
iunss |
⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ↔ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) |
214 |
212 213
|
sylibr |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) |
215 |
208 214
|
unssd |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ⊆ 𝐴 ) |
216 |
|
id |
⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) ) |
217 |
|
iuneq1 |
⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) = ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
218 |
216 217
|
uneq12d |
⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∪ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) |
219 |
218
|
eleq1d |
⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ↔ ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∪ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ) ) |
220 |
|
0elon |
⊢ ∅ ∈ On |
221 |
220
|
elimel |
⊢ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∈ On |
222 |
221
|
elexi |
⊢ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∈ V |
223 |
|
iunon |
⊢ ( ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∈ V ∧ ∀ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) |
224 |
222 223
|
mpan |
⊢ ( ∀ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On → ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) |
225 |
160
|
a1i |
⊢ ( 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) |
226 |
224 225
|
mprg |
⊢ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On |
227 |
221 226
|
onun2i |
⊢ ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∪ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On |
228 |
219 227
|
dedth |
⊢ ( 𝑥 ∈ On → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ) |
229 |
117 228
|
syl |
⊢ ( Lim 𝑥 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ) |
230 |
229
|
adantl |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ) |
231 |
3
|
adantr |
⊢ ( ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) → 𝐴 ∈ On ) |
232 |
|
onsseleq |
⊢ ( ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ⊆ 𝐴 ↔ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) ) ) |
233 |
230 231 232
|
syl2an |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ⊆ 𝐴 ↔ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) ) ) |
234 |
215 233
|
mpbid |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) ) |
235 |
234
|
orcomd |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ) ) |
236 |
235
|
ord |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ¬ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ) ) |
237 |
206 236
|
mpd |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ) |
238 |
137
|
ad2antrl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( card ‘ 𝐴 ) = 𝐴 ) |
239 |
|
iscard |
⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 ) ) |
240 |
239
|
simprbi |
⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ∀ 𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 ) |
241 |
|
breq1 |
⊢ ( 𝑧 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑧 ≺ 𝐴 ↔ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) ) |
242 |
241
|
rspccv |
⊢ ( ∀ 𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) ) |
243 |
238 240 242
|
3syl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) ) |
244 |
237 243
|
mpd |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) |
245 |
|
domsdomtr |
⊢ ( ( ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) |
246 |
107 244 245
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) |
247 |
246
|
exp43 |
⊢ ( 𝑥 ∈ 𝐴 → ( Lim 𝑥 → ( 𝐴 ∈ Inacc → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) ) ) |
248 |
247
|
com4l |
⊢ ( Lim 𝑥 → ( 𝐴 ∈ Inacc → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) ) ) |
249 |
13 17 21 28 61 248
|
tfinds2 |
⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ Inacc → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) ) |
250 |
249
|
impd |
⊢ ( 𝑥 ∈ On → ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) |
251 |
9 250
|
mpcom |
⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) |
252 |
|
sdomdom |
⊢ ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 ) |
253 |
251 252
|
syl |
⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 ) |
254 |
253
|
ralrimiva |
⊢ ( 𝐴 ∈ Inacc → ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 ) |
255 |
|
iundom |
⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 ) → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝐴 × 𝐴 ) ) |
256 |
3 254 255
|
syl2anc |
⊢ ( 𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝐴 × 𝐴 ) ) |
257 |
7 256
|
eqbrtrd |
⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ) |
258 |
|
winainf |
⊢ ( 𝐴 ∈ Inaccw → ω ⊆ 𝐴 ) |
259 |
1 258
|
syl |
⊢ ( 𝐴 ∈ Inacc → ω ⊆ 𝐴 ) |
260 |
|
infxpen |
⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 ) |
261 |
3 259 260
|
syl2anc |
⊢ ( 𝐴 ∈ Inacc → ( 𝐴 × 𝐴 ) ≈ 𝐴 ) |
262 |
|
domentr |
⊢ ( ( ( 𝑅1 ‘ 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ≼ 𝐴 ) |
263 |
257 261 262
|
syl2anc |
⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≼ 𝐴 ) |
264 |
|
fvex |
⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V |
265 |
122
|
fdmi |
⊢ dom 𝑅1 = On |
266 |
2 265
|
eleqtrrdi |
⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1 ) |
267 |
|
onssr1 |
⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) ) |
268 |
1 266 267
|
3syl |
⊢ ( 𝐴 ∈ Inacc → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) ) |
269 |
|
ssdomg |
⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) → 𝐴 ≼ ( 𝑅1 ‘ 𝐴 ) ) ) |
270 |
264 268 269
|
mpsyl |
⊢ ( 𝐴 ∈ Inacc → 𝐴 ≼ ( 𝑅1 ‘ 𝐴 ) ) |
271 |
|
sbth |
⊢ ( ( ( 𝑅1 ‘ 𝐴 ) ≼ 𝐴 ∧ 𝐴 ≼ ( 𝑅1 ‘ 𝐴 ) ) → ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 ) |
272 |
263 270 271
|
syl2anc |
⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 ) |