This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunfictbso

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)

Ref Expression
Assertion iunfictbso ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴 ) → ∪ 𝐴 ≼ ω )

Proof

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 ffvelcdmd ⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ 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 ffvelcdmda ⊢ ( ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ 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 ffvelcdmd ⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ 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 ffvelcdmd ⊢ ( ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ 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 biimtrid ⊢ ( ( ( 𝐴 ≼ ω ∧ 𝐴 ⊆ 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 ∪ 𝐴 ) → ∪ 𝐴 ≼ ω )