| Step |
Hyp |
Ref |
Expression |
| 1 |
|
omex |
⊢ ω ∈ V |
| 2 |
1
|
0dom |
⊢ ∅ ≼ ω |
| 3 |
|
breq1 |
⊢ ( ∪ 𝐴 = ∅ → ( ∪ 𝐴 ≼ ω ↔ ∅ ≼ ω ) ) |
| 4 |
2 3
|
mpbiri |
⊢ ( ∪ 𝐴 = ∅ → ∪ 𝐴 ≼ ω ) |
| 5 |
4
|
a1d |
⊢ ( ∪ 𝐴 = ∅ → ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) → ∪ 𝐴 ≼ ω ) ) |
| 6 |
|
n0 |
⊢ ( ∪ 𝐴 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ ∪ 𝐴 ) |
| 7 |
|
ne0i |
⊢ ( 𝑎 ∈ ∪ 𝐴 → ∪ 𝐴 ≠ ∅ ) |
| 8 |
|
unieq |
⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ ) |
| 9 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
| 10 |
8 9
|
eqtrdi |
⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ ) |
| 11 |
10
|
necon3i |
⊢ ( ∪ 𝐴 ≠ ∅ → 𝐴 ≠ ∅ ) |
| 12 |
7 11
|
syl |
⊢ ( 𝑎 ∈ ∪ 𝐴 → 𝐴 ≠ ∅ ) |
| 13 |
12
|
adantl |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → 𝐴 ≠ ∅ ) |
| 14 |
|
simpl1 |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → 𝐴 ≼ ω ) |
| 15 |
|
ctex |
⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V ) |
| 16 |
|
0sdomg |
⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
| 17 |
14 15 16
|
3syl |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
| 18 |
13 17
|
mpbird |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → ∅ ≺ 𝐴 ) |
| 19 |
|
fodomr |
⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ω ) → ∃ 𝑏 𝑏 : ω –onto→ 𝐴 ) |
| 20 |
18 14 19
|
syl2anc |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → ∃ 𝑏 𝑏 : ω –onto→ 𝐴 ) |
| 21 |
|
omelon |
⊢ ω ∈ On |
| 22 |
|
onenon |
⊢ ( ω ∈ On → ω ∈ dom card ) |
| 23 |
21 22
|
ax-mp |
⊢ ω ∈ dom card |
| 24 |
|
xpnum |
⊢ ( ( ω ∈ dom card ∧ ω ∈ dom card ) → ( ω × ω ) ∈ dom card ) |
| 25 |
23 23 24
|
mp2an |
⊢ ( ω × ω ) ∈ dom card |
| 26 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → 𝑏 : ω –onto→ 𝐴 ) |
| 27 |
|
fof |
⊢ ( 𝑏 : ω –onto→ 𝐴 → 𝑏 : ω ⟶ 𝐴 ) |
| 28 |
26 27
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → 𝑏 : ω ⟶ 𝐴 ) |
| 29 |
|
simprl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → 𝑓 ∈ ω ) |
| 30 |
28 29
|
ffvelrnd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ( 𝑏 ‘ 𝑓 ) ∈ 𝐴 ) |
| 31 |
30
|
adantr |
⊢ ( ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) ∧ 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ) → ( 𝑏 ‘ 𝑓 ) ∈ 𝐴 ) |
| 32 |
|
elssuni |
⊢ ( ( 𝑏 ‘ 𝑓 ) ∈ 𝐴 → ( 𝑏 ‘ 𝑓 ) ⊆ ∪ 𝐴 ) |
| 33 |
31 32
|
syl |
⊢ ( ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) ∧ 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ) → ( 𝑏 ‘ 𝑓 ) ⊆ ∪ 𝐴 ) |
| 34 |
30 32
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ( 𝑏 ‘ 𝑓 ) ⊆ ∪ 𝐴 ) |
| 35 |
|
simpll3 |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → 𝐵 Or ∪ 𝐴 ) |
| 36 |
|
soss |
⊢ ( ( 𝑏 ‘ 𝑓 ) ⊆ ∪ 𝐴 → ( 𝐵 Or ∪ 𝐴 → 𝐵 Or ( 𝑏 ‘ 𝑓 ) ) ) |
| 37 |
34 35 36
|
sylc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → 𝐵 Or ( 𝑏 ‘ 𝑓 ) ) |
| 38 |
|
simpll2 |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → 𝐴 ⊆ Fin ) |
| 39 |
38 30
|
sseldd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ( 𝑏 ‘ 𝑓 ) ∈ Fin ) |
| 40 |
|
finnisoeu |
⊢ ( ( 𝐵 Or ( 𝑏 ‘ 𝑓 ) ∧ ( 𝑏 ‘ 𝑓 ) ∈ Fin ) → ∃! ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) |
| 41 |
37 39 40
|
syl2anc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ∃! ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) |
| 42 |
|
iotacl |
⊢ ( ∃! ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ∈ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) } ) |
| 43 |
41 42
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ∈ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) } ) |
| 44 |
|
iotaex |
⊢ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ∈ V |
| 45 |
|
isoeq1 |
⊢ ( 𝑎 = ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) → ( 𝑎 Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ) |
| 46 |
|
isoeq1 |
⊢ ( ℎ = 𝑎 → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ 𝑎 Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ) |
| 47 |
46
|
cbvabv |
⊢ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) } = { 𝑎 ∣ 𝑎 Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) } |
| 48 |
44 45 47
|
elab2 |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ∈ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) } ↔ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) |
| 49 |
43 48
|
sylib |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) |
| 50 |
|
isof1o |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑓 ) ) –1-1-onto→ ( 𝑏 ‘ 𝑓 ) ) |
| 51 |
|
f1of |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑓 ) ) –1-1-onto→ ( 𝑏 ‘ 𝑓 ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ⟶ ( 𝑏 ‘ 𝑓 ) ) |
| 52 |
49 50 51
|
3syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ⟶ ( 𝑏 ‘ 𝑓 ) ) |
| 53 |
52
|
ffvelrnda |
⊢ ( ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) ∧ 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ) → ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) ∈ ( 𝑏 ‘ 𝑓 ) ) |
| 54 |
33 53
|
sseldd |
⊢ ( ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) ∧ 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ) → ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) ∈ ∪ 𝐴 ) |
| 55 |
|
simprl |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → 𝑎 ∈ ∪ 𝐴 ) |
| 56 |
55
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) ∧ ¬ 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ) → 𝑎 ∈ ∪ 𝐴 ) |
| 57 |
54 56
|
ifclda |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑓 ∈ ω ∧ 𝑔 ∈ ω ) ) → if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ∈ ∪ 𝐴 ) |
| 58 |
57
|
ralrimivva |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ∀ 𝑓 ∈ ω ∀ 𝑔 ∈ ω if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ∈ ∪ 𝐴 ) |
| 59 |
|
eqid |
⊢ ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) = ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) |
| 60 |
59
|
fmpo |
⊢ ( ∀ 𝑓 ∈ ω ∀ 𝑔 ∈ ω if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ∈ ∪ 𝐴 ↔ ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) : ( ω × ω ) ⟶ ∪ 𝐴 ) |
| 61 |
58 60
|
sylib |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) : ( ω × ω ) ⟶ ∪ 𝐴 ) |
| 62 |
|
eluni |
⊢ ( 𝑐 ∈ ∪ 𝐴 ↔ ∃ 𝑖 ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) |
| 63 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → 𝑏 : ω –onto→ 𝐴 ) |
| 64 |
|
simprr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → 𝑖 ∈ 𝐴 ) |
| 65 |
|
foelrn |
⊢ ( ( 𝑏 : ω –onto→ 𝐴 ∧ 𝑖 ∈ 𝐴 ) → ∃ 𝑗 ∈ ω 𝑖 = ( 𝑏 ‘ 𝑗 ) ) |
| 66 |
63 64 65
|
syl2anc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → ∃ 𝑗 ∈ ω 𝑖 = ( 𝑏 ‘ 𝑗 ) ) |
| 67 |
|
simprrl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑗 ∈ ω ) |
| 68 |
|
ordom |
⊢ Ord ω |
| 69 |
|
simpll2 |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝐴 ⊆ Fin ) |
| 70 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑏 : ω –onto→ 𝐴 ) |
| 71 |
70 27
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑏 : ω ⟶ 𝐴 ) |
| 72 |
71 67
|
ffvelrnd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( 𝑏 ‘ 𝑗 ) ∈ 𝐴 ) |
| 73 |
69 72
|
sseldd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( 𝑏 ‘ 𝑗 ) ∈ Fin ) |
| 74 |
|
ficardom |
⊢ ( ( 𝑏 ‘ 𝑗 ) ∈ Fin → ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ∈ ω ) |
| 75 |
73 74
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ∈ ω ) |
| 76 |
|
ordelss |
⊢ ( ( Ord ω ∧ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ∈ ω ) → ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ⊆ ω ) |
| 77 |
68 75 76
|
sylancr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ⊆ ω ) |
| 78 |
|
elssuni |
⊢ ( ( 𝑏 ‘ 𝑗 ) ∈ 𝐴 → ( 𝑏 ‘ 𝑗 ) ⊆ ∪ 𝐴 ) |
| 79 |
72 78
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( 𝑏 ‘ 𝑗 ) ⊆ ∪ 𝐴 ) |
| 80 |
|
simpll3 |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝐵 Or ∪ 𝐴 ) |
| 81 |
|
soss |
⊢ ( ( 𝑏 ‘ 𝑗 ) ⊆ ∪ 𝐴 → ( 𝐵 Or ∪ 𝐴 → 𝐵 Or ( 𝑏 ‘ 𝑗 ) ) ) |
| 82 |
79 80 81
|
sylc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝐵 Or ( 𝑏 ‘ 𝑗 ) ) |
| 83 |
|
finnisoeu |
⊢ ( ( 𝐵 Or ( 𝑏 ‘ 𝑗 ) ∧ ( 𝑏 ‘ 𝑗 ) ∈ Fin ) → ∃! ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) |
| 84 |
82 73 83
|
syl2anc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ∃! ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) |
| 85 |
|
iotacl |
⊢ ( ∃! ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ∈ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) } ) |
| 86 |
84 85
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ∈ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) } ) |
| 87 |
|
iotaex |
⊢ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ∈ V |
| 88 |
|
isoeq1 |
⊢ ( 𝑎 = ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) → ( 𝑎 Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ↔ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 89 |
|
isoeq1 |
⊢ ( ℎ = 𝑎 → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ↔ 𝑎 Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 90 |
89
|
cbvabv |
⊢ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) } = { 𝑎 ∣ 𝑎 Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) } |
| 91 |
87 88 90
|
elab2 |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ∈ { ℎ ∣ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) } ↔ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) |
| 92 |
86 91
|
sylib |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) |
| 93 |
|
isof1o |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑗 ) ) –1-1-onto→ ( 𝑏 ‘ 𝑗 ) ) |
| 94 |
92 93
|
syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑗 ) ) –1-1-onto→ ( 𝑏 ‘ 𝑗 ) ) |
| 95 |
|
f1ocnv |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑗 ) ) –1-1-onto→ ( 𝑏 ‘ 𝑗 ) → ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( 𝑏 ‘ 𝑗 ) –1-1-onto→ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) |
| 96 |
|
f1of |
⊢ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( 𝑏 ‘ 𝑗 ) –1-1-onto→ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) → ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( 𝑏 ‘ 𝑗 ) ⟶ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) |
| 97 |
94 95 96
|
3syl |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( 𝑏 ‘ 𝑗 ) ⟶ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) |
| 98 |
|
simprll |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑐 ∈ 𝑖 ) |
| 99 |
|
simprrr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑖 = ( 𝑏 ‘ 𝑗 ) ) |
| 100 |
98 99
|
eleqtrd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑐 ∈ ( 𝑏 ‘ 𝑗 ) ) |
| 101 |
97 100
|
ffvelrnd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) |
| 102 |
77 101
|
sseldd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ω ) |
| 103 |
|
2fveq3 |
⊢ ( 𝑓 = 𝑗 → ( card ‘ ( 𝑏 ‘ 𝑓 ) ) = ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) |
| 104 |
103
|
eleq2d |
⊢ ( 𝑓 = 𝑗 → ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) ↔ 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 105 |
|
isoeq4 |
⊢ ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) = ( card ‘ ( 𝑏 ‘ 𝑗 ) ) → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ) |
| 106 |
103 105
|
syl |
⊢ ( 𝑓 = 𝑗 → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ) |
| 107 |
|
fveq2 |
⊢ ( 𝑓 = 𝑗 → ( 𝑏 ‘ 𝑓 ) = ( 𝑏 ‘ 𝑗 ) ) |
| 108 |
|
isoeq5 |
⊢ ( ( 𝑏 ‘ 𝑓 ) = ( 𝑏 ‘ 𝑗 ) → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 109 |
107 108
|
syl |
⊢ ( 𝑓 = 𝑗 → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 110 |
106 109
|
bitrd |
⊢ ( 𝑓 = 𝑗 → ( ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ↔ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 111 |
110
|
iotabidv |
⊢ ( 𝑓 = 𝑗 → ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) = ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 112 |
111
|
fveq1d |
⊢ ( 𝑓 = 𝑗 → ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) = ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑔 ) ) |
| 113 |
104 112
|
ifbieq1d |
⊢ ( 𝑓 = 𝑗 → if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) = if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) |
| 114 |
|
eleq1 |
⊢ ( 𝑔 = ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) → ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ↔ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) ) ) |
| 115 |
|
fveq2 |
⊢ ( 𝑔 = ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) → ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑔 ) = ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) ) |
| 116 |
114 115
|
ifbieq1d |
⊢ ( 𝑔 = ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) → if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑔 ) , 𝑎 ) = if ( ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) , 𝑎 ) ) |
| 117 |
|
fvex |
⊢ ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) ∈ V |
| 118 |
|
vex |
⊢ 𝑎 ∈ V |
| 119 |
117 118
|
ifex |
⊢ if ( ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) , 𝑎 ) ∈ V |
| 120 |
113 116 59 119
|
ovmpo |
⊢ ( ( 𝑗 ∈ ω ∧ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ω ) → ( 𝑗 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) = if ( ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) , 𝑎 ) ) |
| 121 |
67 102 120
|
syl2anc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( 𝑗 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) = if ( ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) , 𝑎 ) ) |
| 122 |
101
|
iftrued |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → if ( ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) , 𝑎 ) = ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) ) |
| 123 |
|
f1ocnvfv2 |
⊢ ( ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) : ( card ‘ ( 𝑏 ‘ 𝑗 ) ) –1-1-onto→ ( 𝑏 ‘ 𝑗 ) ∧ 𝑐 ∈ ( 𝑏 ‘ 𝑗 ) ) → ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) = 𝑐 ) |
| 124 |
94 100 123
|
syl2anc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) = 𝑐 ) |
| 125 |
121 122 124
|
3eqtrrd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → 𝑐 = ( 𝑗 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) ) |
| 126 |
|
rspceov |
⊢ ( ( 𝑗 ∈ ω ∧ ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ∈ ω ∧ 𝑐 = ( 𝑗 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) ( ◡ ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑗 ) ) , ( 𝑏 ‘ 𝑗 ) ) ) ‘ 𝑐 ) ) ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) |
| 127 |
67 102 125 126
|
syl3anc |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) ) ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) |
| 128 |
127
|
expr |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → ( ( 𝑗 ∈ ω ∧ 𝑖 = ( 𝑏 ‘ 𝑗 ) ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) |
| 129 |
128
|
expd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → ( 𝑗 ∈ ω → ( 𝑖 = ( 𝑏 ‘ 𝑗 ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) ) |
| 130 |
129
|
rexlimdv |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → ( ∃ 𝑗 ∈ ω 𝑖 = ( 𝑏 ‘ 𝑗 ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) |
| 131 |
66 130
|
mpd |
⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) ∧ ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) |
| 132 |
131
|
ex |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ( ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) |
| 133 |
132
|
exlimdv |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ( ∃ 𝑖 ( 𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴 ) → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) |
| 134 |
62 133
|
syl5bi |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ( 𝑐 ∈ ∪ 𝐴 → ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) |
| 135 |
134
|
ralrimiv |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ∀ 𝑐 ∈ ∪ 𝐴 ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) |
| 136 |
|
foov |
⊢ ( ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) : ( ω × ω ) –onto→ ∪ 𝐴 ↔ ( ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) : ( ω × ω ) ⟶ ∪ 𝐴 ∧ ∀ 𝑐 ∈ ∪ 𝐴 ∃ 𝑑 ∈ ω ∃ 𝑒 ∈ ω 𝑐 = ( 𝑑 ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) 𝑒 ) ) ) |
| 137 |
61 135 136
|
sylanbrc |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) : ( ω × ω ) –onto→ ∪ 𝐴 ) |
| 138 |
|
fodomnum |
⊢ ( ( ω × ω ) ∈ dom card → ( ( 𝑓 ∈ ω , 𝑔 ∈ ω ↦ if ( 𝑔 ∈ ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( ( ℩ ℎ ℎ Isom E , 𝐵 ( ( card ‘ ( 𝑏 ‘ 𝑓 ) ) , ( 𝑏 ‘ 𝑓 ) ) ) ‘ 𝑔 ) , 𝑎 ) ) : ( ω × ω ) –onto→ ∪ 𝐴 → ∪ 𝐴 ≼ ( ω × ω ) ) ) |
| 139 |
25 137 138
|
mpsyl |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ∪ 𝐴 ≼ ( ω × ω ) ) |
| 140 |
|
xpomen |
⊢ ( ω × ω ) ≈ ω |
| 141 |
|
domentr |
⊢ ( ( ∪ 𝐴 ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ∪ 𝐴 ≼ ω ) |
| 142 |
139 140 141
|
sylancl |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ ( 𝑎 ∈ ∪ 𝐴 ∧ 𝑏 : ω –onto→ 𝐴 ) ) → ∪ 𝐴 ≼ ω ) |
| 143 |
142
|
expr |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → ( 𝑏 : ω –onto→ 𝐴 → ∪ 𝐴 ≼ ω ) ) |
| 144 |
143
|
exlimdv |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → ( ∃ 𝑏 𝑏 : ω –onto→ 𝐴 → ∪ 𝐴 ≼ ω ) ) |
| 145 |
20 144
|
mpd |
⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) ∧ 𝑎 ∈ ∪ 𝐴 ) → ∪ 𝐴 ≼ ω ) |
| 146 |
145
|
expcom |
⊢ ( 𝑎 ∈ ∪ 𝐴 → ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) → ∪ 𝐴 ≼ ω ) ) |
| 147 |
146
|
exlimiv |
⊢ ( ∃ 𝑎 𝑎 ∈ ∪ 𝐴 → ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) → ∪ 𝐴 ≼ ω ) ) |
| 148 |
6 147
|
sylbi |
⊢ ( ∪ 𝐴 ≠ ∅ → ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) → ∪ 𝐴 ≼ ω ) ) |
| 149 |
5 148
|
pm2.61ine |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) → ∪ 𝐴 ≼ ω ) |