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

Theorem iunfictbso 9326
 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 8892 . . . . 5 ω ∈ V
210dom 8435 . . . 4 ∅ ≼ ω
3 breq1 4926 . . . 4 ( 𝐴 = ∅ → ( 𝐴 ≼ ω ↔ ∅ ≼ ω))
42, 3mpbiri 250 . . 3 ( 𝐴 = ∅ → 𝐴 ≼ ω)
54a1d 25 . 2 ( 𝐴 = ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
6 n0 4191 . . 3 ( 𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 𝐴)
7 ne0i 4181 . . . . . . . . . 10 (𝑎 𝐴 𝐴 ≠ ∅)
8 unieq 4714 . . . . . . . . . . . 12 (𝐴 = ∅ → 𝐴 = ∅)
9 uni0 4733 . . . . . . . . . . . 12 ∅ = ∅
108, 9syl6eq 2824 . . . . . . . . . . 11 (𝐴 = ∅ → 𝐴 = ∅)
1110necon3i 2993 . . . . . . . . . 10 ( 𝐴 ≠ ∅ → 𝐴 ≠ ∅)
127, 11syl 17 . . . . . . . . 9 (𝑎 𝐴𝐴 ≠ ∅)
1312adantl 474 . . . . . . . 8 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → 𝐴 ≠ ∅)
14 simpl1 1171 . . . . . . . . 9 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → 𝐴 ≼ ω)
15 ctex 8313 . . . . . . . . 9 (𝐴 ≼ ω → 𝐴 ∈ V)
16 0sdomg 8434 . . . . . . . . 9 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1714, 15, 163syl 18 . . . . . . . 8 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → (∅ ≺ 𝐴𝐴 ≠ ∅))
1813, 17mpbird 249 . . . . . . 7 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → ∅ ≺ 𝐴)
19 fodomr 8456 . . . . . . 7 ((∅ ≺ 𝐴𝐴 ≼ ω) → ∃𝑏 𝑏:ω–onto𝐴)
2018, 14, 19syl2anc 576 . . . . . 6 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → ∃𝑏 𝑏:ω–onto𝐴)
21 omelon 8895 . . . . . . . . . . . 12 ω ∈ On
22 onenon 9164 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
2321, 22ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
24 xpnum 9166 . . . . . . . . . . 11 ((ω ∈ dom card ∧ ω ∈ dom card) → (ω × ω) ∈ dom card)
2523, 23, 24mp2an 679 . . . . . . . . . 10 (ω × ω) ∈ dom card
26 simplrr 765 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto𝐴)
27 fof 6413 . . . . . . . . . . . . . . . . . . 19 (𝑏:ω–onto𝐴𝑏:ω⟶𝐴)
2826, 27syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴)
29 simprl 758 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω)
3028, 29ffvelrnd 6671 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏𝑓) ∈ 𝐴)
3130adantr 473 . . . . . . . . . . . . . . . 16 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → (𝑏𝑓) ∈ 𝐴)
32 elssuni 4735 . . . . . . . . . . . . . . . 16 ((𝑏𝑓) ∈ 𝐴 → (𝑏𝑓) ⊆ 𝐴)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → (𝑏𝑓) ⊆ 𝐴)
3430, 32syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏𝑓) ⊆ 𝐴)
35 simpll3 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or 𝐴)
36 soss 5338 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑓) ⊆ 𝐴 → (𝐵 Or 𝐴𝐵 Or (𝑏𝑓)))
3734, 35, 36sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏𝑓))
38 simpll2 1193 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin)
3938, 30sseldd 3855 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏𝑓) ∈ Fin)
40 finnisoeu 9325 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 Or (𝑏𝑓) ∧ (𝑏𝑓) ∈ Fin) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
4137, 39, 40syl2anc 576 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
42 iotacl 6169 . . . . . . . . . . . . . . . . . . 19 (∃! Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))})
4341, 42syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))})
44 iotaex 6163 . . . . . . . . . . . . . . . . . . 19 (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ V
45 isoeq1 6887 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))))
46 isoeq1 6887 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑎 → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))))
4746cbvabv 2904 . . . . . . . . . . . . . . . . . . 19 { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))} = {𝑎𝑎 Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))}
4844, 45, 47elab2 3579 . . . . . . . . . . . . . . . . . 18 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))} ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
4943, 48sylib 210 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))
50 isof1o 6893 . . . . . . . . . . . . . . . . 17 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))–1-1-onto→(𝑏𝑓))
51 f1of 6438 . . . . . . . . . . . . . . . . 17 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))–1-1-onto→(𝑏𝑓) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))⟶(𝑏𝑓))
5249, 50, 513syl 18 . . . . . . . . . . . . . . . 16 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))):(card‘(𝑏𝑓))⟶(𝑏𝑓))
5352ffvelrnda 6670 . . . . . . . . . . . . . . 15 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔) ∈ (𝑏𝑓))
5433, 53sseldd 3855 . . . . . . . . . . . . . 14 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏𝑓))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔) ∈ 𝐴)
55 simprl 758 . . . . . . . . . . . . . . 15 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → 𝑎 𝐴)
5655ad2antrr 713 . . . . . . . . . . . . . 14 (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏𝑓))) → 𝑎 𝐴)
5754, 56ifclda 4378 . . . . . . . . . . . . 13 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) ∈ 𝐴)
5857ralrimivva 3135 . . . . . . . . . . . 12 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) ∈ 𝐴)
59 eqid 2772 . . . . . . . . . . . . 13 (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))
6059fmpo 7567 . . . . . . . . . . . 12 (∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) ∈ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶ 𝐴)
6158, 60sylib 210 . . . . . . . . . . 11 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶ 𝐴)
62 eluni 4709 . . . . . . . . . . . . 13 (𝑐 𝐴 ↔ ∃𝑖(𝑐𝑖𝑖𝐴))
63 simplrr 765 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → 𝑏:ω–onto𝐴)
64 simprr 760 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → 𝑖𝐴)
65 foelrn 6689 . . . . . . . . . . . . . . . . 17 ((𝑏:ω–onto𝐴𝑖𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏𝑗))
6663, 64, 65syl2anc 576 . . . . . . . . . . . . . . . 16 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏𝑗))
67 simprrl 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑗 ∈ ω)
68 ordom 7399 . . . . . . . . . . . . . . . . . . . . . 22 Ord ω
69 simpll2 1193 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝐴 ⊆ Fin)
70 simplrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑏:ω–onto𝐴)
7170, 27syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑏:ω⟶𝐴)
7271, 67ffvelrnd 6671 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑏𝑗) ∈ 𝐴)
7369, 72sseldd 3855 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑏𝑗) ∈ Fin)
74 ficardom 9176 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑗) ∈ Fin → (card‘(𝑏𝑗)) ∈ ω)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (card‘(𝑏𝑗)) ∈ ω)
76 ordelss 6039 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord ω ∧ (card‘(𝑏𝑗)) ∈ ω) → (card‘(𝑏𝑗)) ⊆ ω)
7768, 75, 76sylancr 578 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (card‘(𝑏𝑗)) ⊆ ω)
78 elssuni 4735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑗) ∈ 𝐴 → (𝑏𝑗) ⊆ 𝐴)
7972, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑏𝑗) ⊆ 𝐴)
80 simpll3 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝐵 Or 𝐴)
81 soss 5338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏𝑗) ⊆ 𝐴 → (𝐵 Or 𝐴𝐵 Or (𝑏𝑗)))
8279, 80, 81sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝐵 Or (𝑏𝑗))
83 finnisoeu 9325 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 Or (𝑏𝑗) ∧ (𝑏𝑗) ∈ Fin) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
8482, 73, 83syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ∃! Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
85 iotacl 6169 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃! Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))})
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))})
87 iotaex 6163 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ V
88 isoeq1 6887 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
89 isoeq1 6887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( = 𝑎 → ( Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
9089cbvabv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))} = {𝑎𝑎 Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))}
9187, 88, 90elab2 3579 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) ∈ { Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))} ↔ (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
9286, 91sylib 210 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))
93 isof1o 6893 . . . . . . . . . . . . . . . . . . . . . . . 24 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))) Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗))
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗))
95 f1ocnv 6450 . . . . . . . . . . . . . . . . . . . . . . 23 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)–1-1-onto→(card‘(𝑏𝑗)))
96 f1of 6438 . . . . . . . . . . . . . . . . . . . . . . 23 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)–1-1-onto→(card‘(𝑏𝑗)) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)⟶(card‘(𝑏𝑗)))
9794, 95, 963syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(𝑏𝑗)⟶(card‘(𝑏𝑗)))
98 simprll 766 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑐𝑖)
99 simprrr 769 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑖 = (𝑏𝑗))
10098, 99eleqtrd 2862 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑐 ∈ (𝑏𝑗))
10197, 100ffvelrnd 6671 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)))
10277, 101sseldd 3855 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ ω)
103 2fveq3 6498 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑗 → (card‘(𝑏𝑓)) = (card‘(𝑏𝑗)))
104103eleq2d 2845 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏𝑓)) ↔ 𝑔 ∈ (card‘(𝑏𝑗))))
105 isoeq4 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘(𝑏𝑓)) = (card‘(𝑏𝑗)) → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓))))
106103, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑗 → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓))))
107 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 = 𝑗 → (𝑏𝑓) = (𝑏𝑗))
108 isoeq5 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏𝑓) = (𝑏𝑗) → ( Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑗 → ( Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
110106, 109bitrd 271 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑗 → ( Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)) ↔ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
111110iotabidv 6167 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑗 → (℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓))) = (℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))))
112111fveq1d 6495 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑗 → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔) = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔))
113104, 112ifbieq1d 4367 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔), 𝑎))
114 eleq1 2847 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏𝑗)) ↔ ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗))))
115 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔) = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)))
116114, 115ifbieq1d 4367 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑔), 𝑎) = if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎))
117 fvex 6506 . . . . . . . . . . . . . . . . . . . . . . . 24 ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) ∈ V
118 vex 3412 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑎 ∈ V
119117, 118ifex 4392 . . . . . . . . . . . . . . . . . . . . . . 23 if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎) ∈ V
120113, 116, 59, 119ovmpo 7120 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ ω ∧ ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ ω) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎))
12167, 102, 120syl2anc 576 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎))
122101iftrued 4352 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → if(((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ (card‘(𝑏𝑗)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)), 𝑎) = ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)))
123 f1ocnvfv2 6853 . . . . . . . . . . . . . . . . . . . . . 22 (((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗))):(card‘(𝑏𝑗))–1-1-onto→(𝑏𝑗) ∧ 𝑐 ∈ (𝑏𝑗)) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = 𝑐)
12494, 100, 123syl2anc 576 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)) = 𝑐)
125121, 122, 1243eqtrrd 2813 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐)))
126 rspceov 7016 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ω ∧ ((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))((℩ Isom E , 𝐵 ((card‘(𝑏𝑗)), (𝑏𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
12767, 102, 125, 126syl3anc 1351 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ ((𝑐𝑖𝑖𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
128127expr 449 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
129128expd 408 . . . . . . . . . . . . . . . . 17 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))))
130129rexlimdv 3222 . . . . . . . . . . . . . . . 16 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → (∃𝑗 ∈ ω 𝑖 = (𝑏𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
13166, 130mpd 15 . . . . . . . . . . . . . . 15 ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) ∧ (𝑐𝑖𝑖𝐴)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
132131ex 405 . . . . . . . . . . . . . 14 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → ((𝑐𝑖𝑖𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
133132exlimdv 1892 . . . . . . . . . . . . 13 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (∃𝑖(𝑐𝑖𝑖𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
13462, 133syl5bi 234 . . . . . . . . . . . 12 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (𝑐 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
135134ralrimiv 3125 . . . . . . . . . . 11 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → ∀𝑐 𝐴𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒))
136 foov 7132 . . . . . . . . . . 11 ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶ 𝐴 ∧ ∀𝑐 𝐴𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎))𝑒)))
13761, 135, 136sylanbrc 575 . . . . . . . . . 10 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto 𝐴)
138 fodomnum 9269 . . . . . . . . . 10 ((ω × ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏𝑓)), ((℩ Isom E , 𝐵 ((card‘(𝑏𝑓)), (𝑏𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto 𝐴 𝐴 ≼ (ω × ω)))
13925, 137, 138mpsyl 68 . . . . . . . . 9 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → 𝐴 ≼ (ω × ω))
140 xpomen 9227 . . . . . . . . 9 (ω × ω) ≈ ω
141 domentr 8357 . . . . . . . . 9 (( 𝐴 ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → 𝐴 ≼ ω)
142139, 140, 141sylancl 577 . . . . . . . 8 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ (𝑎 𝐴𝑏:ω–onto𝐴)) → 𝐴 ≼ ω)
143142expr 449 . . . . . . 7 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → (𝑏:ω–onto𝐴 𝐴 ≼ ω))
144143exlimdv 1892 . . . . . 6 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → (∃𝑏 𝑏:ω–onto𝐴 𝐴 ≼ ω))
14520, 144mpd 15 . . . . 5 (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) ∧ 𝑎 𝐴) → 𝐴 ≼ ω)
146145expcom 406 . . . 4 (𝑎 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
147146exlimiv 1889 . . 3 (∃𝑎 𝑎 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
1486, 147sylbi 209 . 2 ( 𝐴 ≠ ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω))
1495, 148pm2.61ine 3045 1 ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or 𝐴) → 𝐴 ≼ ω)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507  ∃wex 1742   ∈ wcel 2048  ∃!weu 2579  {cab 2753   ≠ wne 2961  ∀wral 3082  ∃wrex 3083  Vcvv 3409   ⊆ wss 3825  ∅c0 4173  ifcif 4344  ∪ cuni 4706   class class class wbr 4923   E cep 5309   Or wor 5318   × cxp 5398  ◡ccnv 5399  dom cdm 5400  Ord word 6022  Oncon0 6023  ℩cio 6144  ⟶wf 6178  –onto→wfo 6180  –1-1-onto→wf1o 6181  ‘cfv 6182   Isom wiso 6183  (class class class)co 6970   ∈ cmpo 6972  ωcom 7390   ≈ cen 8295   ≼ cdom 8296   ≺ csdm 8297  Fincfn 8298  cardccrd 9150 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8890 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-oadd 7901  df-omul 7902  df-er 8081  df-map 8200  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-oi 8761  df-card 9154  df-acn 9157 This theorem is referenced by:  aannenlem3  24612
 Copyright terms: Public domain W3C validator