Metamath Proof Explorer

Theorem isomenndlem

Description: O is sub-additive w.r.t. countable indexed union, implies that O is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of Fremlin1 p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses isomenndlem.o ⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
isomenndlem.o0 ⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
isomenndlem.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝒫 𝑋 )
isomenndlem.subadd ⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
isomenndlem.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
isomenndlem.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑌 )
isomenndlem.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
Assertion isomenndlem ( 𝜑 → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 isomenndlem.o ⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
2 isomenndlem.o0 ⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
3 isomenndlem.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝒫 𝑋 )
4 isomenndlem.subadd ⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
5 isomenndlem.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
6 isomenndlem.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝑌 )
7 isomenndlem.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
8 id ⊢ ( 𝜑 → 𝜑 )
9 iftrue ⊢ ( 𝑛 ∈ 𝐵 → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ( 𝐹 ‘ 𝑛 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ( 𝐹 ‘ 𝑛 ) )
11 f1of ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑌 → 𝐹 : 𝐵 ⟶ 𝑌 )
12 6 11 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝑌 )
13 ssun1 ⊢ 𝑌 ⊆ ( 𝑌 ∪ { ∅ } )
14 13 a1i ⊢ ( 𝜑 → 𝑌 ⊆ ( 𝑌 ∪ { ∅ } ) )
15 12 14 fssd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 𝑌 ∪ { ∅ } ) )
16 15 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑌 ∪ { ∅ } ) )
17 10 16 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ ( 𝑌 ∪ { ∅ } ) )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ ( 𝑌 ∪ { ∅ } ) )
19 iffalse ⊢ ( ¬ 𝑛 ∈ 𝐵 → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ∅ )
20 19 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ∅ )
21 0ex ⊢ ∅ ∈ V
22 21 snid ⊢ ∅ ∈ { ∅ }
23 elun2 ⊢ ( ∅ ∈ { ∅ } → ∅ ∈ ( 𝑌 ∪ { ∅ } ) )
24 22 23 ax-mp ⊢ ∅ ∈ ( 𝑌 ∪ { ∅ } )
25 24 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑛 ∈ 𝐵 ) → ∅ ∈ ( 𝑌 ∪ { ∅ } ) )
26 20 25 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ ( 𝑌 ∪ { ∅ } ) )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ ( 𝑌 ∪ { ∅ } ) )
28 18 27 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ ( 𝑌 ∪ { ∅ } ) )
29 28 7 fmptd ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ ( 𝑌 ∪ { ∅ } ) )
30 0elpw ⊢ ∅ ∈ 𝒫 𝑋
31 snssi ⊢ ( ∅ ∈ 𝒫 𝑋 → { ∅ } ⊆ 𝒫 𝑋 )
32 30 31 ax-mp ⊢ { ∅ } ⊆ 𝒫 𝑋
33 32 a1i ⊢ ( 𝜑 → { ∅ } ⊆ 𝒫 𝑋 )
34 3 33 unssd ⊢ ( 𝜑 → ( 𝑌 ∪ { ∅ } ) ⊆ 𝒫 𝑋 )
35 29 34 fssd ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 𝑋 )
36 nnex ⊢ ℕ ∈ V
37 36 mptex ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ∈ V
38 7 37 eqeltri ⊢ 𝐴 ∈ V
39 feq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 : ℕ ⟶ 𝒫 𝑋 ↔ 𝐴 : ℕ ⟶ 𝒫 𝑋 ) )
40 39 anbi2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) ↔ ( 𝜑 ∧ 𝐴 : ℕ ⟶ 𝒫 𝑋 ) ) )
41 fveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑛 ) )
42 41 iuneq2d ⊢ ( 𝑎 = 𝐴 → ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
43 42 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) )
44 simpl ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ ) → 𝑎 = 𝐴 )
45 44 fveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ ) → ( 𝑎 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑛 ) )
46 45 fveq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) )
47 46 mpteq2dva ⊢ ( 𝑎 = 𝐴 → ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) )
48 47 fveq2d ⊢ ( 𝑎 = 𝐴 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
49 43 48 breq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) ↔ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) )
50 40 49 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) ) ↔ ( ( 𝜑 ∧ 𝐴 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) ) )
51 38 50 4 vtocl ⊢ ( ( 𝜑 ∧ 𝐴 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
52 8 35 51 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
53 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝐹 : 𝐵 ⟶ 𝑌 )
54 simpr ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
55 id ⊢ ( 𝐵 = ℕ → 𝐵 = ℕ )
56 55 eqcomd ⊢ ( 𝐵 = ℕ → ℕ = 𝐵 )
57 56 adantr ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ ℕ ) → ℕ = 𝐵 )
58 54 57 eleqtrd ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ 𝐵 )
59 58 adantll ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ 𝐵 )
60 53 59 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑌 )
61 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) )
62 60 61 fmptd ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) : ℕ ⟶ 𝑌 )
63 7 a1i ⊢ ( 𝐵 = ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) )
64 58 iftrued ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ( 𝐹 ‘ 𝑛 ) )
65 64 mpteq2dva ⊢ ( 𝐵 = ℕ → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) )
66 63 65 eqtrd ⊢ ( 𝐵 = ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) )
67 66 feq1d ⊢ ( 𝐵 = ℕ → ( 𝐴 : ℕ ⟶ 𝑌 ↔ ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) : ℕ ⟶ 𝑌 ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ( 𝐴 : ℕ ⟶ 𝑌 ↔ ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) : ℕ ⟶ 𝑌 ) )
69 62 68 mpbird ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → 𝐴 : ℕ ⟶ 𝑌 )
70 f1ofo ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝑌 → 𝐹 : 𝐵 –onto→ 𝑌 )
71 6 70 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ 𝑌 )
72 dffo3 ⊢ ( 𝐹 : 𝐵 –onto→ 𝑌 ↔ ( 𝐹 : 𝐵 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) ) )
73 71 72 sylib ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) ) )
74 73 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
77 rspa ⊢ ( ( ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) )
78 75 76 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) )
79 78 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) )
80 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝐵 = ℕ )
81 nfre1 ⊢ Ⅎ 𝑛 ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 )
82 simpr ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ 𝐵 )
83 simpl ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → 𝐵 = ℕ )
84 82 83 eleqtrd ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ ℕ )
85 84 adantll ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ ℕ )
86 85 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → 𝑛 ∈ ℕ )
87 63 fveq1d ⊢ ( 𝐵 = ℕ → ( 𝐴 ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ‘ 𝑛 ) )
88 87 3ad2ant1 ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → ( 𝐴 ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ‘ 𝑛 ) )
89 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
90 89 21 ifex ⊢ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ V
91 90 a1i ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ V )
92 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
93 92 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
94 84 91 93 syl2anc ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
95 9 adantl ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ( 𝐹 ‘ 𝑛 ) )
96 94 95 eqtrd ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
97 96 3adant3 ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
98 id ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑛 ) → 𝑦 = ( 𝐹 ‘ 𝑛 ) )
99 98 eqcomd ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑛 ) → ( 𝐹 ‘ 𝑛 ) = 𝑦 )
100 99 3ad2ant3 ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) = 𝑦 )
101 88 97 100 3eqtrrd ⊢ ( ( 𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → 𝑦 = ( 𝐴 ‘ 𝑛 ) )
102 101 3adant1l ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → 𝑦 = ( 𝐴 ‘ 𝑛 ) )
103 rspe ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
104 86 102 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = ( 𝐹 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
105 104 3exp ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ( 𝑛 ∈ 𝐵 → ( 𝑦 = ( 𝐹 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) ) )
106 80 81 105 rexlimd ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ( ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ∃ 𝑛 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
108 79 107 mpd ⊢ ( ( ( 𝜑 ∧ 𝐵 = ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
109 108 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
110 69 109 jca ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ( 𝐴 : ℕ ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
111 dffo3 ⊢ ( 𝐴 : ℕ –onto→ 𝑌 ↔ ( 𝐴 : ℕ ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
112 110 111 sylibr ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → 𝐴 : ℕ –onto→ 𝑌 )
113 founiiun ⊢ ( 𝐴 : ℕ –onto→ 𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
114 112 113 syl ⊢ ( ( 𝜑 ∧ 𝐵 = ℕ ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
115 uniun ⊢ ∪ ( 𝑌 ∪ { ∅ } ) = ( ∪ 𝑌 ∪ ∪ { ∅ } )
116 21 unisn ⊢ ∪ { ∅ } = ∅
117 116 uneq2i ⊢ ( ∪ 𝑌 ∪ ∪ { ∅ } ) = ( ∪ 𝑌 ∪ ∅ )
118 un0 ⊢ ( ∪ 𝑌 ∪ ∅ ) = ∪ 𝑌
119 115 117 118 3eqtrri ⊢ ∪ 𝑌 = ∪ ( 𝑌 ∪ { ∅ } )
120 119 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ∪ 𝑌 = ∪ ( 𝑌 ∪ { ∅ } ) )
121 29 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → 𝐴 : ℕ ⟶ ( 𝑌 ∪ { ∅ } ) )
122 nfv ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 = ∅ )
123 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → 𝐵 ⊆ ℕ )
124 55 necon3bi ⊢ ( ¬ 𝐵 = ℕ → 𝐵 ≠ ℕ )
125 124 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → 𝐵 ≠ ℕ )
126 123 125 jca ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ( 𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ ) )
127 df-pss ⊢ ( 𝐵 ⊊ ℕ ↔ ( 𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ ) )
128 126 127 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → 𝐵 ⊊ ℕ )
129 pssnel ⊢ ( 𝐵 ⊊ ℕ → ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) )
130 128 129 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) )
131 130 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 = ∅ ) → ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) )
132 simprl ⊢ ( ( ( 𝜑 ∧ 𝑦 = ∅ ) ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → 𝑛 ∈ ℕ )
133 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → 𝑛 ∈ ℕ )
134 90 a1i ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ V )
135 7 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ V ) → ( 𝐴 ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
136 133 134 135 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → ( 𝐴 ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
137 136 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 = ∅ ) ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → ( 𝐴 ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
138 19 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑦 = ∅ ) ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ∅ )
139 id ⊢ ( 𝑦 = ∅ → 𝑦 = ∅ )
140 139 eqcomd ⊢ ( 𝑦 = ∅ → ∅ = 𝑦 )
141 140 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 = ∅ ) ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → ∅ = 𝑦 )
142 137 138 141 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 = ∅ ) ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → 𝑦 = ( 𝐴 ‘ 𝑛 ) )
143 132 142 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 = ∅ ) ∧ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
144 143 ex ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
145 144 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 = ∅ ) → ( ( 𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
146 122 81 131 145 exlimimdd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 = ∅ ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
147 146 adantlr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ) ∧ 𝑦 = ∅ ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
148 simplll ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ) ∧ ¬ 𝑦 = ∅ ) → 𝜑 )
149 simpl ⊢ ( ( 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) )
150 elsni ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
151 150 con3i ⊢ ( ¬ 𝑦 = ∅ → ¬ 𝑦 ∈ { ∅ } )
152 151 adantl ⊢ ( ( 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∧ ¬ 𝑦 = ∅ ) → ¬ 𝑦 ∈ { ∅ } )
153 elunnel2 ⊢ ( ( 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∧ ¬ 𝑦 ∈ { ∅ } ) → 𝑦 ∈ 𝑌 )
154 149 152 153 syl2anc ⊢ ( ( 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ∈ 𝑌 )
155 154 adantll ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ∈ 𝑌 )
156 71 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐹 : 𝐵 –onto→ 𝑌 )
157 foelrni ⊢ ( ( 𝐹 : 𝐵 –onto→ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ 𝐵 ( 𝐹 ‘ 𝑛 ) = 𝑦 )
158 156 76 157 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ 𝐵 ( 𝐹 ‘ 𝑛 ) = 𝑦 )
159 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑦 ∈ 𝑌 )
160 5 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ ℕ )
161 160 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑦 ) → 𝑛 ∈ ℕ )
162 160 90 135 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
163 162 10 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
164 163 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑦 ) → ( 𝐴 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
165 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑦 ) → ( 𝐹 ‘ 𝑛 ) = 𝑦 )
166 164 165 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑦 ) → 𝑦 = ( 𝐴 ‘ 𝑛 ) )
167 161 166 103 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
168 167 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐵 → ( ( 𝐹 ‘ 𝑛 ) = 𝑦 → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑛 ∈ 𝐵 → ( ( 𝐹 ‘ 𝑛 ) = 𝑦 → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) ) )
170 159 81 169 rexlimd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ∃ 𝑛 ∈ 𝐵 ( 𝐹 ‘ 𝑛 ) = 𝑦 → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
171 158 170 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
172 148 155 171 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ) ∧ ¬ 𝑦 = ∅ ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
173 147 172 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) ∧ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
174 173 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ∀ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) )
175 121 174 jca ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ( 𝐴 : ℕ ⟶ ( 𝑌 ∪ { ∅ } ) ∧ ∀ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
176 dffo3 ⊢ ( 𝐴 : ℕ –onto→ ( 𝑌 ∪ { ∅ } ) ↔ ( 𝐴 : ℕ ⟶ ( 𝑌 ∪ { ∅ } ) ∧ ∀ 𝑦 ∈ ( 𝑌 ∪ { ∅ } ) ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝐴 ‘ 𝑛 ) ) )
177 175 176 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → 𝐴 : ℕ –onto→ ( 𝑌 ∪ { ∅ } ) )
178 founiiun ⊢ ( 𝐴 : ℕ –onto→ ( 𝑌 ∪ { ∅ } ) → ∪ ( 𝑌 ∪ { ∅ } ) = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
179 177 178 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ∪ ( 𝑌 ∪ { ∅ } ) = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
180 120 179 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ℕ ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
181 114 180 pm2.61dan ⊢ ( 𝜑 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) )
182 181 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑌 ) = ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) )
183 uncom ⊢ ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐵 ∪ ( ℕ ∖ 𝐵 ) )
184 183 a1i ⊢ ( 𝜑 → ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐵 ∪ ( ℕ ∖ 𝐵 ) ) )
185 undif ⊢ ( 𝐵 ⊆ ℕ ↔ ( 𝐵 ∪ ( ℕ ∖ 𝐵 ) ) = ℕ )
186 5 185 sylib ⊢ ( 𝜑 → ( 𝐵 ∪ ( ℕ ∖ 𝐵 ) ) = ℕ )
187 184 186 eqtrd ⊢ ( 𝜑 → ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) = ℕ )
188 187 eqcomd ⊢ ( 𝜑 → ℕ = ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) )
189 188 mpteq1d ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) )
190 189 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
191 nfv ⊢ Ⅎ 𝑛 𝜑
192 difexg ⊢ ( ℕ ∈ V → ( ℕ ∖ 𝐵 ) ∈ V )
193 36 192 ax-mp ⊢ ( ℕ ∖ 𝐵 ) ∈ V
194 193 a1i ⊢ ( 𝜑 → ( ℕ ∖ 𝐵 ) ∈ V )
195 36 a1i ⊢ ( 𝜑 → ℕ ∈ V )
196 195 5 ssexd ⊢ ( 𝜑 → 𝐵 ∈ V )
197 incom ⊢ ( ( ℕ ∖ 𝐵 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( ℕ ∖ 𝐵 ) )
198 disjdif ⊢ ( 𝐵 ∩ ( ℕ ∖ 𝐵 ) ) = ∅
199 197 198 eqtri ⊢ ( ( ℕ ∖ 𝐵 ) ∩ 𝐵 ) = ∅
200 199 a1i ⊢ ( 𝜑 → ( ( ℕ ∖ 𝐵 ) ∩ 𝐵 ) = ∅ )
201 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → 𝜑 )
202 eldifi ⊢ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) → 𝑛 ∈ ℕ )
203 202 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → 𝑛 ∈ ℕ )
204 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
205 35 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
206 204 205 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
207 201 203 206 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
208 160 206 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
209 191 194 196 200 207 208 sge0splitmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( ( ℕ ∖ 𝐵 ) ∪ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) )
210 eqid ⊢ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) )
211 208 210 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
212 196 211 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
213 212 xaddid2d ⊢ ( 𝜑 → ( 0 +𝑒 ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
214 90 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) ∈ V )
215 203 214 135 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ( 𝐴 ‘ 𝑛 ) = if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) )
216 eldifn ⊢ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) → ¬ 𝑛 ∈ 𝐵 )
217 216 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ¬ 𝑛 ∈ 𝐵 )
218 217 iffalsed ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → if ( 𝑛 ∈ 𝐵 , ( 𝐹 ‘ 𝑛 ) , ∅ ) = ∅ )
219 215 218 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ( 𝐴 ‘ 𝑛 ) = ∅ )
220 219 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∅ ) )
221 201 2 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ( 𝑂 ‘ ∅ ) = 0 )
222 220 221 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ 𝐵 ) ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) = 0 )
223 222 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ 0 ) )
224 223 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ 0 ) ) )
225 191 194 sge0z ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ 0 ) ) = 0 )
226 224 225 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) = 0 )
227 226 oveq1d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) = ( 0 +𝑒 ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) )
228 1 3 feqresmpt ⊢ ( 𝜑 → ( 𝑂 ↾ 𝑌 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑂 ‘ 𝑦 ) ) )
229 228 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑌 ↦ ( 𝑂 ‘ 𝑦 ) ) ) )
230 nfv ⊢ Ⅎ 𝑦 𝜑
231 fveq2 ⊢ ( 𝑦 = ( 𝐴 ‘ 𝑛 ) → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) )
232 163 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑛 ) )
233 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
234 3 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝒫 𝑋 )
235 233 234 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑂 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
236 230 191 231 196 6 232 235 sge0f1o ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ 𝑌 ↦ ( 𝑂 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
237 eqidd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
238 229 236 237 3eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
239 213 227 238 3eqtr4d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑛 ∈ ( ℕ ∖ 𝐵 ) ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑛 ∈ 𝐵 ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) = ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) )
240 190 209 239 3eqtrrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) )
241 182 240 breq12d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) ↔ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) ) )
242 52 241 mpbird ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) )