Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunfictbso Structured version   Visualization version   GIF version

Theorem iunfictbso 9147
 Description: Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Assertion
Ref Expression
iunfictbso ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω)

Proof of Theorem iunfictbso
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omex 8715 . . . . 5 ω ∈ V
210dom 8257 . . . 4 ∅ ≼ ω
3 breq1 4807 . . . 4 ( 𝐴 = ∅ → ( 𝐴 ≼ ω ↔ ∅ ≼ ω))
42, 3mpbiri 248 . . 3 ( 𝐴 = ∅ → 𝐴 ≼ ω)
54a1d 25 . 2 ( 𝐴 = ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
6 n0 4074 . . 3 ( 𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 𝐴)
7 ne0i 4064 . . . . . . . . . 10 (𝑎 𝐴 𝐴 ≠ ∅)
8 unieq 4596 . . . . . . . . . . . 12 (𝐴 = ∅ → 𝐴 = ∅)
9 uni0 4617 . . . . . . . . . . . 12 ∅ = ∅
108, 9syl6eq 2810 . . . . . . . . . . 11 (𝐴 = ∅ → 𝐴 = ∅)
1110necon3i 2964 . . . . . . . . . 10 ( 𝐴 ≠ ∅ → 𝐴 ≠ ∅)
127, 11syl 17 . . . . . . . . 9 (𝑎 𝐴𝐴 ≠ ∅)
1312adantl 473 . . . . . . . 8 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → 𝐴 ≠ ∅)
14 simpl1 1228 . . . . . . . . 9 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → 𝐴 ≼ ω)
15 reldom 8129 . . . . . . . . . 10 Rel ≼
1615brrelexi 5315 . . . . . . . . 9 (𝐴 ≼ ω → 𝐴 ∈ V)
17 0sdomg 8256 . . . . . . . . 9 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1814, 16, 173syl 18 . . . . . . . 8 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → (∅ ≺ 𝐴𝐴 ≠ ∅))
1913, 18mpbird 247 . . . . . . 7 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → ∅ ≺ 𝐴)
20 fodomr 8278 . . . . . . 7 ((∅ ≺ 𝐴𝐴 ≼ ω) → ∃𝑏 𝑏:ω–onto𝐴)
2119, 14, 20syl2anc 696 . . . . . 6 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → ∃𝑏 𝑏:ω–onto𝐴)
22 omelon 8718 . . . . . . . . . . . 12 ω ∈ On
23 onenon 8985 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
2422, 23ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
25 xpnum 8987 . . . . . . . . . . 11 ((ω ∈ dom card ∧ ω ∈ dom card) → (ω × ω) ∈ dom card)
2624, 24, 25mp2an 710 . . . . . . . . . 10 (ω × ω) ∈ dom card
27 simplrr 820 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto𝐴)
28 fof 6277 . . . . . . . . . . . . . . . . . . 19 (𝑏:ω–onto𝐴𝑏:ω⟶𝐴)
2927, 28syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴)
30 simprl 811 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω)
3129, 30ffvelrnd 6524 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏𝑓) ∈ 𝐴)
3231adantr 472 . . . . . . . . . . . . . . . 16 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → (𝑏𝑓) ∈ 𝐴)
33 elssuni 4619 . . . . . . . . . . . . . . . 16 ((𝑏𝑓) ∈ 𝐴 → (𝑏𝑓) ⊆ 𝐴)
3432, 33syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → (𝑏𝑓) ⊆ 𝐴)
3531, 33syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏𝑓) ⊆ 𝐴)
36 simpll3 1259 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or 𝐴)
37 soss 5205 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑓) ⊆ 𝐴 → (𝐵 Or 𝐴𝐵 Or (𝑏𝑓)))
3835, 36, 37sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏𝑓))
39 simpll2 1257 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin)
4039, 31sseldd 3745 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏𝑓) ∈ Fin)
41 finnisoeu 9146 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 Or (𝑏𝑓) ∧ (𝑏𝑓) ∈ Fin) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
4238, 40, 41syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
43 iotacl 6035 . . . . . . . . . . . . . . . . . . 19 (∃! Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))})
4442, 43syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))})
45 iotaex 6029 . . . . . . . . . . . . . . . . . . 19 (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ V
46 isoeq1 6731 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))))
47 isoeq1 6731 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑎 → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))))
4847cbvabv 2885 . . . . . . . . . . . . . . . . . . 19 { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))} = {𝑎𝑎 Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))}
4945, 46, 48elab2 3494 . . . . . . . . . . . . . . . . . 18 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))} ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
5044, 49sylib 208 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
51 isof1o 6737 . . . . . . . . . . . . . . . . 17 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))–1-1-onto→(𝑏𝑓))
52 f1of 6299 . . . . . . . . . . . . . . . . 17 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))–1-1-onto→(𝑏𝑓) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))⟶(𝑏𝑓))
5350, 51, 523syl 18 . . . . . . . . . . . . . . . 16 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))⟶(𝑏𝑓))
5453ffvelrnda 6523 . . . . . . . . . . . . . . 15 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔) ∈ (𝑏𝑓))
5534, 54sseldd 3745 . . . . . . . . . . . . . 14 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔) ∈ 𝐴)
56 simprl 811 . . . . . . . . . . . . . . 15 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → 𝑎 𝐴)
5756ad2antrr 764 . . . . . . . . . . . . . 14 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏𝑓))) → 𝑎 𝐴)
5855, 57ifclda 4264 . . . . . . . . . . . . 13 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) ∈ 𝐴)
5958ralrimivva 3109 . . . . . . . . . . . 12 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) ∈ 𝐴)
60 eqid 2760 . . . . . . . . . . . . 13 (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))
6160fmpt2 7406 . . . . . . . . . . . 12 (∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) ∈ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶ 𝐴)
6259, 61sylib 208 . . . . . . . . . . 11 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶ 𝐴)
63 eluni 4591 . . . . . . . . . . . . 13 (𝑐 𝐴 ↔ ∃𝑖(𝑐𝑖𝑖𝐴))
64 simplrr 820 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → 𝑏:ω–onto𝐴)
65 simprr 813 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → 𝑖𝐴)
66 foelrn 6542 . . . . . . . . . . . . . . . . 17 ((𝑏:ω–onto𝐴𝑖𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏𝑗))
6764, 65, 66syl2anc 696 . . . . . . . . . . . . . . . 16 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏𝑗))
68 simprrl 823 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑗 ∈ ω)
69 ordom 7240 . . . . . . . . . . . . . . . . . . . . . 22 Ord ω
70 simpll2 1257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝐴 ⊆ Fin)
71 simplrr 820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑏:ω–onto𝐴)
7271, 28syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑏:ω⟶𝐴)
7372, 68ffvelrnd 6524 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑏𝑗) ∈ 𝐴)
7470, 73sseldd 3745 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑏𝑗) ∈ Fin)
75 ficardom 8997 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑗) ∈ Fin → (card‘(𝑏𝑗)) ∈ ω)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (card‘(𝑏𝑗)) ∈ ω)
77 ordelss 5900 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord ω ∧ (card‘(𝑏𝑗)) ∈ ω) → (card‘(𝑏𝑗)) ⊆ ω)
7869, 76, 77sylancr 698 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (card‘(𝑏𝑗)) ⊆ ω)
79 elssuni 4619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑗) ∈ 𝐴 → (𝑏𝑗) ⊆ 𝐴)
8073, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑏𝑗) ⊆ 𝐴)
81 simpll3 1259 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝐵 Or 𝐴)
82 soss 5205 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏𝑗) ⊆ 𝐴 → (𝐵 Or 𝐴𝐵 Or (𝑏𝑗)))
8380, 81, 82sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝐵 Or (𝑏𝑗))
84 finnisoeu 9146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 Or (𝑏𝑗) ∧ (𝑏𝑗) ∈ Fin) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
8583, 74, 84syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
86 iotacl 6035 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃! Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))})
8785, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))})
88 iotaex 6029 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ V
89 isoeq1 6731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
90 isoeq1 6731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( = 𝑎 → ( Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
9190cbvabv 2885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))} = {𝑎𝑎 Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))}
9288, 89, 91elab2 3494 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))} ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
9387, 92sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
94 isof1o 6737 . . . . . . . . . . . . . . . . . . . . . . . 24 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗))
9593, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗))
96 f1ocnv 6311 . . . . . . . . . . . . . . . . . . . . . . 23 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)–1-1-onto→(card‘(𝑏𝑗)))
97 f1of 6299 . . . . . . . . . . . . . . . . . . . . . . 23 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)–1-1-onto→(card‘(𝑏𝑗)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)⟶(card‘(𝑏𝑗)))
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)⟶(card‘(𝑏𝑗)))
99 simprll 821 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑐𝑖)
100 simprrr 824 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑖 = (𝑏𝑗))
10199, 100eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑐 ∈ (𝑏𝑗))
10298, 101ffvelrnd 6524 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)))
10378, 102sseldd 3745 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ ω)
104 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑗 → (𝑏𝑓) = (𝑏𝑗))
105104fveq2d 6357 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑗 → (card‘(𝑏𝑓)) = (card‘(𝑏𝑗)))
106105eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏𝑓)) ↔ 𝑔 ∈ (card‘(𝑏𝑗))))
107 isoeq4 6734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘(𝑏𝑓)) = (card‘(𝑏𝑗)) → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓))))
108105, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑗 → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓))))
109 isoeq5 6735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏𝑓) = (𝑏𝑗) → ( Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
110104, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑗 → ( Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
111108, 110bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑗 → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
112111iotabidv 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑗 → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) = (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
113112fveq1d 6355 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑗 → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔) = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔))
114106, 113ifbieq1d 4253 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔), 𝑎))
115 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏𝑗)) ↔ ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗))))
116 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔) = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)))
117115, 116ifbieq1d 4253 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔), 𝑎) = if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎))
118 fvex 6363 . . . . . . . . . . . . . . . . . . . . . . . 24 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) ∈ V
119 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑎 ∈ V
120118, 119ifex 4300 . . . . . . . . . . . . . . . . . . . . . . 23 if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎) ∈ V
121114, 117, 60, 120ovmpt2 6962 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ω ∧ ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ ω) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎))
12268, 103, 121syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎))
123102iftrued 4238 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎) = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)))
124 f1ocnvfv2 6697 . . . . . . . . . . . . . . . . . . . . . 22 (((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗) ∧ 𝑐 ∈ (𝑏𝑗)) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = 𝑐)
12595, 101, 124syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = 𝑐)
126122, 123, 1253eqtrrd 2799 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)))
127 rspceov 6856 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ω ∧ ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
12868, 103, 126, 127syl3anc 1477 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
129128expr 644 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
130129expd 451 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))))
131130rexlimdv 3168 . . . . . . . . . . . . . . . 16 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → (∃𝑗 ∈ ω 𝑖 = (𝑏𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
13267, 131mpd 15 . . . . . . . . . . . . . . 15 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
133132ex 449 . . . . . . . . . . . . . 14 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → ((𝑐𝑖𝑖𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
134133exlimdv 2010 . . . . . . . . . . . . 13 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (∃𝑖(𝑐𝑖𝑖𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
13563, 134syl5bi 232 . . . . . . . . . . . 12 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (𝑐 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
136135ralrimiv 3103 . . . . . . . . . . 11 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → ∀𝑐 𝐴𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
137 foov 6974 . . . . . . . . . . 11 ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶ 𝐴 ∧ ∀𝑐 𝐴𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
13862, 136, 137sylanbrc 701 . . . . . . . . . 10 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto 𝐴)
139 fodomnum 9090 . . . . . . . . . 10 ((ω × ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto 𝐴 𝐴 ≼ (ω × ω)))
14026, 138, 139mpsyl 68 . . . . . . . . 9 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → 𝐴 ≼ (ω × ω))
141 xpomen 9048 . . . . . . . . 9 (ω × ω) ≈ ω
142 domentr 8182 . . . . . . . . 9 (( 𝐴 ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → 𝐴 ≼ ω)
143140, 141, 142sylancl 697 . . . . . . . 8 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → 𝐴 ≼ ω)
144143expr 644 . . . . . . 7 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → (𝑏:ω–onto𝐴 𝐴 ≼ ω))
145144exlimdv 2010 . . . . . 6 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → (∃𝑏 𝑏:ω–onto𝐴 𝐴 ≼ ω))
14621, 145mpd 15 . . . . 5 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → 𝐴 ≼ ω)
147146expcom 450 . . . 4 (𝑎 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
148147exlimiv 2007 . . 3 (∃𝑎 𝑎 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
1496, 148sylbi 207 . 2 ( 𝐴 ≠ ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
1505, 149pm2.61ine 3015 1 ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∃!weu 2607  {cab 2746   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  Vcvv 3340   ⊆ wss 3715  ∅c0 4058  ifcif 4230  ∪ cuni 4588   class class class wbr 4804   E cep 5178   Or wor 5186   × cxp 5264  ◡ccnv 5265  dom cdm 5266  Ord word 5883  Oncon0 5884  ℩cio 6010  ⟶wf 6045  –onto→wfo 6047  –1-1-onto→wf1o 6048  ‘cfv 6049   Isom wiso 6050  (class class class)co 6814   ↦ cmpt2 6816  ωcom 7231   ≈ cen 8120   ≼ cdom 8121   ≺ csdm 8122  Fincfn 8123  cardccrd 8971 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-omul 7735  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-oi 8582  df-card 8975  df-acn 8978 This theorem is referenced by:  aannenlem3  24304
 Copyright terms: Public domain W3C validator