Step |
Hyp |
Ref |
Expression |
1 |
|
dfac12.1 |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
2 |
|
dfac12.3 |
⊢ ( 𝜑 → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On ) |
3 |
|
dfac12.4 |
⊢ 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ) |
4 |
|
dfac12.5 |
⊢ ( 𝜑 → 𝐶 ∈ On ) |
5 |
|
dfac12.h |
⊢ 𝐻 = ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) |
6 |
|
dfac12.6 |
⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 ) |
7 |
|
dfac12.8 |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) |
8 |
3
|
tfr1 |
⊢ 𝐺 Fn On |
9 |
|
fnfun |
⊢ ( 𝐺 Fn On → Fun 𝐺 ) |
10 |
8 9
|
ax-mp |
⊢ Fun 𝐺 |
11 |
|
funimaexg |
⊢ ( ( Fun 𝐺 ∧ 𝐶 ∈ On ) → ( 𝐺 “ 𝐶 ) ∈ V ) |
12 |
10 4 11
|
sylancr |
⊢ ( 𝜑 → ( 𝐺 “ 𝐶 ) ∈ V ) |
13 |
|
uniexg |
⊢ ( ( 𝐺 “ 𝐶 ) ∈ V → ∪ ( 𝐺 “ 𝐶 ) ∈ V ) |
14 |
|
rnexg |
⊢ ( ∪ ( 𝐺 “ 𝐶 ) ∈ V → ran ∪ ( 𝐺 “ 𝐶 ) ∈ V ) |
15 |
12 13 14
|
3syl |
⊢ ( 𝜑 → ran ∪ ( 𝐺 “ 𝐶 ) ∈ V ) |
16 |
|
f1f |
⊢ ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On → ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) ⟶ On ) |
17 |
|
fssxp |
⊢ ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) ⟶ On → ( 𝐺 ‘ 𝑧 ) ⊆ ( ( 𝑅1 ‘ 𝑧 ) × On ) ) |
18 |
|
ssv |
⊢ ( 𝑅1 ‘ 𝑧 ) ⊆ V |
19 |
|
xpss1 |
⊢ ( ( 𝑅1 ‘ 𝑧 ) ⊆ V → ( ( 𝑅1 ‘ 𝑧 ) × On ) ⊆ ( V × On ) ) |
20 |
18 19
|
ax-mp |
⊢ ( ( 𝑅1 ‘ 𝑧 ) × On ) ⊆ ( V × On ) |
21 |
|
sstr |
⊢ ( ( ( 𝐺 ‘ 𝑧 ) ⊆ ( ( 𝑅1 ‘ 𝑧 ) × On ) ∧ ( ( 𝑅1 ‘ 𝑧 ) × On ) ⊆ ( V × On ) ) → ( 𝐺 ‘ 𝑧 ) ⊆ ( V × On ) ) |
22 |
20 21
|
mpan2 |
⊢ ( ( 𝐺 ‘ 𝑧 ) ⊆ ( ( 𝑅1 ‘ 𝑧 ) × On ) → ( 𝐺 ‘ 𝑧 ) ⊆ ( V × On ) ) |
23 |
|
fvex |
⊢ ( 𝐺 ‘ 𝑧 ) ∈ V |
24 |
23
|
elpw |
⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ↔ ( 𝐺 ‘ 𝑧 ) ⊆ ( V × On ) ) |
25 |
22 24
|
sylibr |
⊢ ( ( 𝐺 ‘ 𝑧 ) ⊆ ( ( 𝑅1 ‘ 𝑧 ) × On ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ) |
26 |
16 17 25
|
3syl |
⊢ ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On → ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ) |
27 |
26
|
ralimi |
⊢ ( ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On → ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ) |
28 |
7 27
|
syl |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ) |
29 |
|
onss |
⊢ ( 𝐶 ∈ On → 𝐶 ⊆ On ) |
30 |
4 29
|
syl |
⊢ ( 𝜑 → 𝐶 ⊆ On ) |
31 |
8
|
fndmi |
⊢ dom 𝐺 = On |
32 |
30 31
|
sseqtrrdi |
⊢ ( 𝜑 → 𝐶 ⊆ dom 𝐺 ) |
33 |
|
funimass4 |
⊢ ( ( Fun 𝐺 ∧ 𝐶 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝐶 ) ⊆ 𝒫 ( V × On ) ↔ ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ) ) |
34 |
10 32 33
|
sylancr |
⊢ ( 𝜑 → ( ( 𝐺 “ 𝐶 ) ⊆ 𝒫 ( V × On ) ↔ ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) ∈ 𝒫 ( V × On ) ) ) |
35 |
28 34
|
mpbird |
⊢ ( 𝜑 → ( 𝐺 “ 𝐶 ) ⊆ 𝒫 ( V × On ) ) |
36 |
|
sspwuni |
⊢ ( ( 𝐺 “ 𝐶 ) ⊆ 𝒫 ( V × On ) ↔ ∪ ( 𝐺 “ 𝐶 ) ⊆ ( V × On ) ) |
37 |
35 36
|
sylib |
⊢ ( 𝜑 → ∪ ( 𝐺 “ 𝐶 ) ⊆ ( V × On ) ) |
38 |
|
rnss |
⊢ ( ∪ ( 𝐺 “ 𝐶 ) ⊆ ( V × On ) → ran ∪ ( 𝐺 “ 𝐶 ) ⊆ ran ( V × On ) ) |
39 |
37 38
|
syl |
⊢ ( 𝜑 → ran ∪ ( 𝐺 “ 𝐶 ) ⊆ ran ( V × On ) ) |
40 |
|
rnxpss |
⊢ ran ( V × On ) ⊆ On |
41 |
39 40
|
sstrdi |
⊢ ( 𝜑 → ran ∪ ( 𝐺 “ 𝐶 ) ⊆ On ) |
42 |
|
ssonuni |
⊢ ( ran ∪ ( 𝐺 “ 𝐶 ) ∈ V → ( ran ∪ ( 𝐺 “ 𝐶 ) ⊆ On → ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ) ) |
43 |
15 41 42
|
sylc |
⊢ ( 𝜑 → ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ) |
44 |
|
suceloni |
⊢ ( ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On → suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ) |
45 |
43 44
|
syl |
⊢ ( 𝜑 → suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ) |
46 |
45
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ) |
47 |
|
rankon |
⊢ ( rank ‘ 𝑦 ) ∈ On |
48 |
|
omcl |
⊢ ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ∧ ( rank ‘ 𝑦 ) ∈ On ) → ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) ∈ On ) |
49 |
46 47 48
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) ∈ On ) |
50 |
|
fveq2 |
⊢ ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ) |
51 |
|
f1eq1 |
⊢ ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) ) |
52 |
50 51
|
syl |
⊢ ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) ) |
53 |
|
fveq2 |
⊢ ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( 𝑅1 ‘ 𝑧 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
54 |
|
f1eq2 |
⊢ ( ( 𝑅1 ‘ 𝑧 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) ) |
55 |
53 54
|
syl |
⊢ ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) ) |
56 |
52 55
|
bitrd |
⊢ ( 𝑧 = suc ( rank ‘ 𝑦 ) → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) ) |
57 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) |
58 |
|
rankr1ai |
⊢ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 ) |
59 |
58
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ 𝐶 ) |
60 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → 𝐶 = ∪ 𝐶 ) |
61 |
59 60
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 ) |
62 |
|
eloni |
⊢ ( 𝐶 ∈ On → Ord 𝐶 ) |
63 |
4 62
|
syl |
⊢ ( 𝜑 → Ord 𝐶 ) |
64 |
63
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → Ord 𝐶 ) |
65 |
|
ordsucuniel |
⊢ ( Ord 𝐶 → ( ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) ) |
66 |
64 65
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( rank ‘ 𝑦 ) ∈ ∪ 𝐶 ↔ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) ) |
67 |
61 66
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) |
68 |
56 57 67
|
rspcdva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) |
69 |
|
f1f |
⊢ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⟶ On ) |
70 |
68 69
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⟶ On ) |
71 |
|
r1elwf |
⊢ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) |
72 |
71
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) |
73 |
|
rankidb |
⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
74 |
72 73
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
75 |
70 74
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ On ) |
76 |
|
oacl |
⊢ ( ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) ∈ On ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ On ) → ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) ∈ On ) |
77 |
49 75 76
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) ∈ On ) |
78 |
|
f1f |
⊢ ( 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ⟶ On ) |
79 |
2 78
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ⟶ On ) |
80 |
79
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ⟶ On ) |
81 |
|
imassrn |
⊢ ( 𝐻 “ 𝑦 ) ⊆ ran 𝐻 |
82 |
|
fvex |
⊢ ( 𝐺 ‘ ∪ 𝐶 ) ∈ V |
83 |
82
|
rnex |
⊢ ran ( 𝐺 ‘ ∪ 𝐶 ) ∈ V |
84 |
|
fveq2 |
⊢ ( 𝑧 = ∪ 𝐶 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ∪ 𝐶 ) ) |
85 |
|
f1eq1 |
⊢ ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ∪ 𝐶 ) → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) ) |
86 |
84 85
|
syl |
⊢ ( 𝑧 = ∪ 𝐶 → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) ) |
87 |
|
fveq2 |
⊢ ( 𝑧 = ∪ 𝐶 → ( 𝑅1 ‘ 𝑧 ) = ( 𝑅1 ‘ ∪ 𝐶 ) ) |
88 |
|
f1eq2 |
⊢ ( ( 𝑅1 ‘ 𝑧 ) = ( 𝑅1 ‘ ∪ 𝐶 ) → ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ On ) ) |
89 |
87 88
|
syl |
⊢ ( 𝑧 = ∪ 𝐶 → ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ On ) ) |
90 |
86 89
|
bitrd |
⊢ ( 𝑧 = ∪ 𝐶 → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ↔ ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ On ) ) |
91 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∀ 𝑧 ∈ 𝐶 ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) |
92 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐶 ∈ On ) |
93 |
|
onuni |
⊢ ( 𝐶 ∈ On → ∪ 𝐶 ∈ On ) |
94 |
|
sucidg |
⊢ ( ∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶 ) |
95 |
92 93 94
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ suc ∪ 𝐶 ) |
96 |
63
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → Ord 𝐶 ) |
97 |
|
orduniorsuc |
⊢ ( Ord 𝐶 → ( 𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶 ) ) |
98 |
96 97
|
syl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → ( 𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶 ) ) |
99 |
98
|
orcanai |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐶 = suc ∪ 𝐶 ) |
100 |
95 99
|
eleqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ 𝐶 ) |
101 |
90 91 100
|
rspcdva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ On ) |
102 |
|
f1f |
⊢ ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ On → ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) ⟶ On ) |
103 |
|
frn |
⊢ ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) ⟶ On → ran ( 𝐺 ‘ ∪ 𝐶 ) ⊆ On ) |
104 |
101 102 103
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ran ( 𝐺 ‘ ∪ 𝐶 ) ⊆ On ) |
105 |
|
epweon |
⊢ E We On |
106 |
|
wess |
⊢ ( ran ( 𝐺 ‘ ∪ 𝐶 ) ⊆ On → ( E We On → E We ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
107 |
104 105 106
|
mpisyl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → E We ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
108 |
|
eqid |
⊢ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) = OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
109 |
108
|
oiiso |
⊢ ( ( ran ( 𝐺 ‘ ∪ 𝐶 ) ∈ V ∧ E We ran ( 𝐺 ‘ ∪ 𝐶 ) ) → OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) Isom E , E ( dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
110 |
83 107 109
|
sylancr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) Isom E , E ( dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
111 |
|
isof1o |
⊢ ( OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) Isom E , E ( dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) , ran ( 𝐺 ‘ ∪ 𝐶 ) ) → OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) –1-1-onto→ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
112 |
|
f1ocnv |
⊢ ( OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) –1-1-onto→ ran ( 𝐺 ‘ ∪ 𝐶 ) → ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : ran ( 𝐺 ‘ ∪ 𝐶 ) –1-1-onto→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
113 |
|
f1of1 |
⊢ ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : ran ( 𝐺 ‘ ∪ 𝐶 ) –1-1-onto→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) → ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : ran ( 𝐺 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
114 |
110 111 112 113
|
4syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : ran ( 𝐺 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
115 |
|
f1f1orn |
⊢ ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ On → ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1-onto→ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
116 |
|
f1of1 |
⊢ ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1-onto→ ran ( 𝐺 ‘ ∪ 𝐶 ) → ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
117 |
101 115 116
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
118 |
|
f1co |
⊢ ( ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) : ran ( 𝐺 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∧ ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ ran ( 𝐺 ‘ ∪ 𝐶 ) ) → ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
119 |
114 117 118
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
120 |
|
f1eq1 |
⊢ ( 𝐻 = ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) → ( 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ↔ ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) ) |
121 |
5 120
|
ax-mp |
⊢ ( 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ↔ ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∘ ( 𝐺 ‘ ∪ 𝐶 ) ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
122 |
119 121
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
123 |
|
f1f |
⊢ ( 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) → 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) ⟶ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
124 |
|
frn |
⊢ ( 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) ⟶ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) → ran 𝐻 ⊆ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
125 |
122 123 124
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ran 𝐻 ⊆ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
126 |
|
harcl |
⊢ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ∈ On |
127 |
126
|
onordi |
⊢ Ord ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) |
128 |
108
|
oion |
⊢ ( ran ( 𝐺 ‘ ∪ 𝐶 ) ∈ V → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∈ On ) |
129 |
83 128
|
mp1i |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∈ On ) |
130 |
108
|
oien |
⊢ ( ( ran ( 𝐺 ‘ ∪ 𝐶 ) ∈ V ∧ E We ran ( 𝐺 ‘ ∪ 𝐶 ) ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ≈ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
131 |
83 107 130
|
sylancr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ≈ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
132 |
|
fvex |
⊢ ( 𝑅1 ‘ ∪ 𝐶 ) ∈ V |
133 |
132
|
f1oen |
⊢ ( ( 𝐺 ‘ ∪ 𝐶 ) : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1-onto→ ran ( 𝐺 ‘ ∪ 𝐶 ) → ( 𝑅1 ‘ ∪ 𝐶 ) ≈ ran ( 𝐺 ‘ ∪ 𝐶 ) ) |
134 |
|
ensym |
⊢ ( ( 𝑅1 ‘ ∪ 𝐶 ) ≈ ran ( 𝐺 ‘ ∪ 𝐶 ) → ran ( 𝐺 ‘ ∪ 𝐶 ) ≈ ( 𝑅1 ‘ ∪ 𝐶 ) ) |
135 |
101 115 133 134
|
4syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ran ( 𝐺 ‘ ∪ 𝐶 ) ≈ ( 𝑅1 ‘ ∪ 𝐶 ) ) |
136 |
|
fvex |
⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V |
137 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐴 ∈ On ) |
138 |
6
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐶 ⊆ 𝐴 ) |
139 |
138 100
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ∪ 𝐶 ∈ 𝐴 ) |
140 |
|
r1ord2 |
⊢ ( 𝐴 ∈ On → ( ∪ 𝐶 ∈ 𝐴 → ( 𝑅1 ‘ ∪ 𝐶 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) ) |
141 |
137 139 140
|
sylc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝑅1 ‘ ∪ 𝐶 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) |
142 |
|
ssdomg |
⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( ( 𝑅1 ‘ ∪ 𝐶 ) ⊆ ( 𝑅1 ‘ 𝐴 ) → ( 𝑅1 ‘ ∪ 𝐶 ) ≼ ( 𝑅1 ‘ 𝐴 ) ) ) |
143 |
136 141 142
|
mpsyl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝑅1 ‘ ∪ 𝐶 ) ≼ ( 𝑅1 ‘ 𝐴 ) ) |
144 |
|
endomtr |
⊢ ( ( ran ( 𝐺 ‘ ∪ 𝐶 ) ≈ ( 𝑅1 ‘ ∪ 𝐶 ) ∧ ( 𝑅1 ‘ ∪ 𝐶 ) ≼ ( 𝑅1 ‘ 𝐴 ) ) → ran ( 𝐺 ‘ ∪ 𝐶 ) ≼ ( 𝑅1 ‘ 𝐴 ) ) |
145 |
135 143 144
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ran ( 𝐺 ‘ ∪ 𝐶 ) ≼ ( 𝑅1 ‘ 𝐴 ) ) |
146 |
|
endomtr |
⊢ ( ( dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ≈ ran ( 𝐺 ‘ ∪ 𝐶 ) ∧ ran ( 𝐺 ‘ ∪ 𝐶 ) ≼ ( 𝑅1 ‘ 𝐴 ) ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ≼ ( 𝑅1 ‘ 𝐴 ) ) |
147 |
131 145 146
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ≼ ( 𝑅1 ‘ 𝐴 ) ) |
148 |
|
elharval |
⊢ ( dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∈ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ↔ ( dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∈ On ∧ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ≼ ( 𝑅1 ‘ 𝐴 ) ) ) |
149 |
129 147 148
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∈ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
150 |
|
ordelss |
⊢ ( ( Ord ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ∧ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∈ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ⊆ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
151 |
127 149 150
|
sylancr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ⊆ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
152 |
125 151
|
sstrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ran 𝐻 ⊆ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
153 |
81 152
|
sstrid |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑦 ) ⊆ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
154 |
|
fvex |
⊢ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ∈ V |
155 |
154
|
elpw2 |
⊢ ( ( 𝐻 “ 𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ↔ ( 𝐻 “ 𝑦 ) ⊆ ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
156 |
153 155
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
157 |
80 156
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ∈ On ) |
158 |
77 157
|
ifclda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ∈ On ) |
159 |
158
|
ex |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ∈ On ) ) |
160 |
|
iftrue |
⊢ ( 𝐶 = ∪ 𝐶 → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) ) |
161 |
|
iftrue |
⊢ ( 𝐶 = ∪ 𝐶 → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) |
162 |
160 161
|
eqeq12d |
⊢ ( 𝐶 = ∪ 𝐶 → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) ) |
163 |
162
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) ) |
164 |
45
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ) |
165 |
|
nsuceq0 |
⊢ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ≠ ∅ |
166 |
165
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ≠ ∅ ) |
167 |
47
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( rank ‘ 𝑦 ) ∈ On ) |
168 |
|
onsucuni |
⊢ ( ran ∪ ( 𝐺 “ 𝐶 ) ⊆ On → ran ∪ ( 𝐺 “ 𝐶 ) ⊆ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
169 |
41 168
|
syl |
⊢ ( 𝜑 → ran ∪ ( 𝐺 “ 𝐶 ) ⊆ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
170 |
169
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ran ∪ ( 𝐺 “ 𝐶 ) ⊆ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
171 |
30
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → 𝐶 ⊆ On ) |
172 |
|
fnfvima |
⊢ ( ( 𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc ( rank ‘ 𝑦 ) ∈ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ∈ ( 𝐺 “ 𝐶 ) ) |
173 |
8 171 67 172
|
mp3an2i |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ∈ ( 𝐺 “ 𝐶 ) ) |
174 |
|
elssuni |
⊢ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ∈ ( 𝐺 “ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ∪ ( 𝐺 “ 𝐶 ) ) |
175 |
|
rnss |
⊢ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ∪ ( 𝐺 “ 𝐶 ) → ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ran ∪ ( 𝐺 “ 𝐶 ) ) |
176 |
173 174 175
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ran ∪ ( 𝐺 “ 𝐶 ) ) |
177 |
|
f1fn |
⊢ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) Fn ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
178 |
68 177
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) Fn ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
179 |
|
fnfvelrn |
⊢ ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) Fn ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ) |
180 |
178 74 179
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ ran ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ) |
181 |
176 180
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ ran ∪ ( 𝐺 “ 𝐶 ) ) |
182 |
170 181
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
183 |
182
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
184 |
|
rankon |
⊢ ( rank ‘ 𝑧 ) ∈ On |
185 |
184
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( rank ‘ 𝑧 ) ∈ On ) |
186 |
|
eleq1w |
⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↔ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) |
187 |
186
|
anbi2d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ↔ ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ) |
188 |
187
|
anbi1d |
⊢ ( 𝑦 = 𝑧 → ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) ) ) |
189 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) |
190 |
|
suceq |
⊢ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑧 ) ) |
191 |
189 190
|
syl |
⊢ ( 𝑦 = 𝑧 → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑧 ) ) |
192 |
191
|
fveq2d |
⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ) |
193 |
|
id |
⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 ) |
194 |
192 193
|
fveq12d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) |
195 |
194
|
eleq1d |
⊢ ( 𝑦 = 𝑧 → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ↔ ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) ) |
196 |
188 195
|
imbi12d |
⊢ ( 𝑦 = 𝑧 → ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) ↔ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) ) ) |
197 |
196 182
|
chvarvv |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
198 |
197
|
adantlrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) |
199 |
|
omopth2 |
⊢ ( ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ∈ On ∧ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ≠ ∅ ) ∧ ( ( rank ‘ 𝑦 ) ∈ On ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) ∧ ( ( rank ‘ 𝑧 ) ∈ On ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ) ) → ( ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ↔ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) ) |
200 |
164 166 167 183 185 198 199
|
syl222anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ↔ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) ) |
201 |
190
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑧 ) ) |
202 |
201
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ) |
203 |
202
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) |
204 |
203
|
eqeq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) ↔ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) |
205 |
68
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) |
206 |
205
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ) |
207 |
74
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
208 |
207
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
209 |
|
r1elwf |
⊢ ( 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) → 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) |
210 |
|
rankidb |
⊢ ( 𝑧 ∈ ∪ ( 𝑅1 “ On ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) ) |
211 |
209 210
|
syl |
⊢ ( 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) ) |
212 |
211
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) ) |
213 |
212
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) ) |
214 |
201
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑧 ) ) ) |
215 |
213 214
|
eleqtrrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) |
216 |
|
f1fveq |
⊢ ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) : ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) –1-1→ On ∧ ( 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ∧ 𝑧 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) ) |
217 |
206 208 215 216
|
syl12anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) ) |
218 |
204 217
|
bitr3d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) ) |
219 |
218
|
biimpd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) ∧ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ) → ( ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) |
220 |
219
|
expimpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) → 𝑦 = 𝑧 ) ) |
221 |
189 194
|
jca |
⊢ ( 𝑦 = 𝑧 → ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ) |
222 |
220 221
|
impbid1 |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) ↔ 𝑦 = 𝑧 ) ) |
223 |
163 200 222
|
3bitrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ 𝐶 = ∪ 𝐶 ) → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) ) |
224 |
|
iffalse |
⊢ ( ¬ 𝐶 = ∪ 𝐶 → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) |
225 |
|
iffalse |
⊢ ( ¬ 𝐶 = ∪ 𝐶 → if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) |
226 |
224 225
|
eqeq12d |
⊢ ( ¬ 𝐶 = ∪ 𝐶 → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ) |
227 |
226
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ) |
228 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On ) |
229 |
156
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
230 |
187
|
anbi1d |
⊢ ( 𝑦 = 𝑧 → ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) ) ) |
231 |
|
imaeq2 |
⊢ ( 𝑦 = 𝑧 → ( 𝐻 “ 𝑦 ) = ( 𝐻 “ 𝑧 ) ) |
232 |
231
|
eleq1d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝐻 “ 𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ↔ ( 𝐻 “ 𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) ) |
233 |
230 232
|
imbi12d |
⊢ ( 𝑦 = 𝑧 → ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) ) ) |
234 |
233 156
|
chvarvv |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
235 |
234
|
adantlrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝐻 “ 𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) |
236 |
|
f1fveq |
⊢ ( ( 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On ∧ ( ( 𝐻 “ 𝑦 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ∧ ( 𝐻 “ 𝑧 ) ∈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) ) ) → ( ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ↔ ( 𝐻 “ 𝑦 ) = ( 𝐻 “ 𝑧 ) ) ) |
237 |
228 229 235 236
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ↔ ( 𝐻 “ 𝑦 ) = ( 𝐻 “ 𝑧 ) ) ) |
238 |
122
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ) |
239 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) |
240 |
99
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝑅1 ‘ 𝐶 ) = ( 𝑅1 ‘ suc ∪ 𝐶 ) ) |
241 |
|
r1suc |
⊢ ( ∪ 𝐶 ∈ On → ( 𝑅1 ‘ suc ∪ 𝐶 ) = 𝒫 ( 𝑅1 ‘ ∪ 𝐶 ) ) |
242 |
92 93 241
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝑅1 ‘ suc ∪ 𝐶 ) = 𝒫 ( 𝑅1 ‘ ∪ 𝐶 ) ) |
243 |
240 242
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝑅1 ‘ 𝐶 ) = 𝒫 ( 𝑅1 ‘ ∪ 𝐶 ) ) |
244 |
243
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( 𝑅1 ‘ 𝐶 ) = 𝒫 ( 𝑅1 ‘ ∪ 𝐶 ) ) |
245 |
239 244
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝑦 ∈ 𝒫 ( 𝑅1 ‘ ∪ 𝐶 ) ) |
246 |
245
|
elpwid |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝑦 ⊆ ( 𝑅1 ‘ ∪ 𝐶 ) ) |
247 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) |
248 |
247 244
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝑧 ∈ 𝒫 ( 𝑅1 ‘ ∪ 𝐶 ) ) |
249 |
248
|
elpwid |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → 𝑧 ⊆ ( 𝑅1 ‘ ∪ 𝐶 ) ) |
250 |
|
f1imaeq |
⊢ ( ( 𝐻 : ( 𝑅1 ‘ ∪ 𝐶 ) –1-1→ dom OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝐶 ) ) ∧ ( 𝑦 ⊆ ( 𝑅1 ‘ ∪ 𝐶 ) ∧ 𝑧 ⊆ ( 𝑅1 ‘ ∪ 𝐶 ) ) ) → ( ( 𝐻 “ 𝑦 ) = ( 𝐻 “ 𝑧 ) ↔ 𝑦 = 𝑧 ) ) |
251 |
238 246 249 250
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( ( 𝐻 “ 𝑦 ) = ( 𝐻 “ 𝑧 ) ↔ 𝑦 = 𝑧 ) ) |
252 |
227 237 251
|
3bitrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) ∧ ¬ 𝐶 = ∪ 𝐶 ) → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) ) |
253 |
223 252
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) ) → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) ) |
254 |
253
|
ex |
⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ∧ 𝑧 ∈ ( 𝑅1 ‘ 𝐶 ) ) → ( if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) = if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑧 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑧 ) ) ‘ 𝑧 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑧 ) ) ) ↔ 𝑦 = 𝑧 ) ) ) |
255 |
159 254
|
dom2lem |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) : ( 𝑅1 ‘ 𝐶 ) –1-1→ On ) |
256 |
1 2 3 4 5
|
dfac12lem1 |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) ) |
257 |
|
f1eq1 |
⊢ ( ( 𝐺 ‘ 𝐶 ) = ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) → ( ( 𝐺 ‘ 𝐶 ) : ( 𝑅1 ‘ 𝐶 ) –1-1→ On ↔ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) : ( 𝑅1 ‘ 𝐶 ) –1-1→ On ) ) |
258 |
256 257
|
syl |
⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐶 ) : ( 𝑅1 ‘ 𝐶 ) –1-1→ On ↔ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐶 ) ↦ if ( 𝐶 = ∪ 𝐶 , ( ( suc ∪ ran ∪ ( 𝐺 “ 𝐶 ) ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝐺 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( 𝐻 “ 𝑦 ) ) ) ) : ( 𝑅1 ‘ 𝐶 ) –1-1→ On ) ) |
259 |
255 258
|
mpbird |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) : ( 𝑅1 ‘ 𝐶 ) –1-1→ On ) |