Metamath Proof Explorer

Theorem imambfm

Description: If the sigma-algebra in the range of a given function is generated by a collection of basic sets K , then to check the measurability of that function, we need only consider inverse images of basic sets a . (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses imambfm.1 ⊢ ( 𝜑 → 𝐾 ∈ V )
imambfm.2 ⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
imambfm.3 ⊢ ( 𝜑 → 𝑇 = ( sigaGen ‘ 𝐾 ) )
Assertion imambfm ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 imambfm.1 ⊢ ( 𝜑 → 𝐾 ∈ V )
2 imambfm.2 ⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
3 imambfm.3 ⊢ ( 𝜑 → 𝑇 = ( sigaGen ‘ 𝐾 ) )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
5 1 sgsiga ⊢ ( 𝜑 → ( sigaGen ‘ 𝐾 ) ∈ ∪ ran sigAlgebra )
6 3 5 eqeltrd ⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) → 𝑇 ∈ ∪ ran sigAlgebra )
8 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
9 4 7 8 mbfmf ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
10 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → 𝑆 ∈ ∪ ran sigAlgebra )
11 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → 𝑇 ∈ ∪ ran sigAlgebra )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
13 sssigagen ⊢ ( 𝐾 ∈ V → 𝐾 ⊆ ( sigaGen ‘ 𝐾 ) )
14 1 13 syl ⊢ ( 𝜑 → 𝐾 ⊆ ( sigaGen ‘ 𝐾 ) )
15 14 3 sseqtrrd ⊢ ( 𝜑 → 𝐾 ⊆ 𝑇 )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → 𝐾 ⊆ 𝑇 )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → 𝑎 ∈ 𝐾 )
18 16 17 sseldd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → 𝑎 ∈ 𝑇 )
19 10 11 12 18 mbfmcnvima ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) ∧ 𝑎 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
20 19 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) → ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
21 9 20 jca ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) → ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) )
22 unielsiga ⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ∪ 𝑇 ∈ 𝑇 )
23 6 22 syl ⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑇 )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∪ 𝑇 ∈ 𝑇 )
25 unielsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆 )
26 2 25 syl ⊢ ( 𝜑 → ∪ 𝑆 ∈ 𝑆 )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∪ 𝑆 ∈ 𝑆 )
28 simprl ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
29 elmapg ⊢ ( ( ∪ 𝑇 ∈ 𝑇 ∧ ∪ 𝑆 ∈ 𝑆 ) → ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ↔ 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ) )
30 29 biimpar ⊢ ( ( ( ∪ 𝑇 ∈ 𝑇 ∧ ∪ 𝑆 ∈ 𝑆 ) ∧ 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ) → 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) )
31 24 27 28 30 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) )
32 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝑇 = ( sigaGen ‘ 𝐾 ) )
33 simpl ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝜑 )
34 ssrab2 ⊢ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝑇
35 pwuni ⊢ 𝑇 ⊆ 𝒫 ∪ 𝑇
36 34 35 sstri ⊢ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝒫 ∪ 𝑇
37 36 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝒫 ∪ 𝑇 )
38 fimacnv ⊢ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 → ( ◡ 𝐹 “ ∪ 𝑇 ) = ∪ 𝑆 )
39 38 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( ◡ 𝐹 “ ∪ 𝑇 ) = ∪ 𝑆 )
40 39 27 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( ◡ 𝐹 “ ∪ 𝑇 ) ∈ 𝑆 )
41 imaeq2 ⊢ ( 𝑎 = ∪ 𝑇 → ( ◡ 𝐹 “ 𝑎 ) = ( ◡ 𝐹 “ ∪ 𝑇 ) )
42 41 eleq1d ⊢ ( 𝑎 = ∪ 𝑇 → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ ∪ 𝑇 ) ∈ 𝑆 ) )
43 42 elrab ⊢ ( ∪ 𝑇 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ( ∪ 𝑇 ∈ 𝑇 ∧ ( ◡ 𝐹 “ ∪ 𝑇 ) ∈ 𝑆 ) )
44 24 40 43 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∪ 𝑇 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
45 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → 𝑇 ∈ ∪ ran sigAlgebra )
46 45 22 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ∪ 𝑇 ∈ 𝑇 )
47 elrabi ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } → 𝑥 ∈ 𝑇 )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → 𝑥 ∈ 𝑇 )
49 difelsiga ⊢ ( ( 𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 ∈ 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 )
50 45 46 48 49 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 )
51 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
52 ffun ⊢ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 → Fun 𝐹 )
53 difpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ∪ 𝑇 ∖ 𝑥 ) ) = ( ( ◡ 𝐹 “ ∪ 𝑇 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
54 51 52 53 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ◡ 𝐹 “ ( ∪ 𝑇 ∖ 𝑥 ) ) = ( ( ◡ 𝐹 “ ∪ 𝑇 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
55 39 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( ( ◡ 𝐹 “ ∪ 𝑇 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) = ( ∪ 𝑆 ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ( ◡ 𝐹 “ ∪ 𝑇 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) = ( ∪ 𝑆 ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
57 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → 𝑆 ∈ ∪ ran sigAlgebra )
58 57 25 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ∪ 𝑆 ∈ 𝑆 )
59 imaeq2 ⊢ ( 𝑎 = 𝑥 → ( ◡ 𝐹 “ 𝑎 ) = ( ◡ 𝐹 “ 𝑥 ) )
60 59 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
61 60 elrab ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ( 𝑥 ∈ 𝑇 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
62 61 simprbi ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 )
63 62 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 )
64 difelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑆 ∈ 𝑆 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝑆 )
65 57 58 63 64 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ∪ 𝑆 ∖ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝑆 )
66 56 65 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ( ◡ 𝐹 “ ∪ 𝑇 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) ∈ 𝑆 )
67 54 66 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ◡ 𝐹 “ ( ∪ 𝑇 ∖ 𝑥 ) ) ∈ 𝑆 )
68 imaeq2 ⊢ ( 𝑎 = ( ∪ 𝑇 ∖ 𝑥 ) → ( ◡ 𝐹 “ 𝑎 ) = ( ◡ 𝐹 “ ( ∪ 𝑇 ∖ 𝑥 ) ) )
69 68 eleq1d ⊢ ( 𝑎 = ( ∪ 𝑇 ∖ 𝑥 ) → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ ( ∪ 𝑇 ∖ 𝑥 ) ) ∈ 𝑆 ) )
70 69 elrab ⊢ ( ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ( ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 ∧ ( ◡ 𝐹 “ ( ∪ 𝑇 ∖ 𝑥 ) ) ∈ 𝑆 ) )
71 50 67 70 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
72 71 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∀ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
73 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → 𝑇 ∈ ∪ ran sigAlgebra )
74 34 sspwi ⊢ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝒫 𝑇
75 74 sseli ⊢ ( 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } → 𝑥 ∈ 𝒫 𝑇 )
76 75 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → 𝑥 ∈ 𝒫 𝑇 )
77 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → 𝑥 ≼ ω )
78 sigaclcu ⊢ ( ( 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑇 )
79 73 76 77 78 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑇 )
80 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) )
81 80 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
82 unipreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ◡ 𝐹 “ 𝑦 ) )
83 81 52 82 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ( ◡ 𝐹 “ ∪ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ◡ 𝐹 “ 𝑦 ) )
84 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → 𝑆 ∈ ∪ ran sigAlgebra )
85 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
86 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
87 elelpwi ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → 𝑦 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
88 85 86 87 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
89 imaeq2 ⊢ ( 𝑎 = 𝑦 → ( ◡ 𝐹 “ 𝑎 ) = ( ◡ 𝐹 “ 𝑦 ) )
90 89 eleq1d ⊢ ( 𝑎 = 𝑦 → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 ) )
91 90 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ( 𝑦 ∈ 𝑇 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 ) )
92 91 simprbi ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 )
93 88 92 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) ∧ 𝑦 ∈ 𝑥 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 )
94 93 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ∀ 𝑦 ∈ 𝑥 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 )
95 nfcv ⊢ Ⅎ 𝑦 𝑥
96 95 sigaclcuni ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑦 ∈ 𝑥 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑦 ∈ 𝑥 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 )
97 84 94 77 96 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ∪ 𝑦 ∈ 𝑥 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 )
98 83 97 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ( ◡ 𝐹 “ ∪ 𝑥 ) ∈ 𝑆 )
99 imaeq2 ⊢ ( 𝑎 = ∪ 𝑥 → ( ◡ 𝐹 “ 𝑎 ) = ( ◡ 𝐹 “ ∪ 𝑥 ) )
100 99 eleq1d ⊢ ( 𝑎 = ∪ 𝑥 → ( ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ ∪ 𝑥 ) ∈ 𝑆 ) )
101 100 elrab ⊢ ( ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ( ∪ 𝑥 ∈ 𝑇 ∧ ( ◡ 𝐹 “ ∪ 𝑥 ) ∈ 𝑆 ) )
102 79 98 101 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
103 102 ex ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) )
104 103 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∀ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) )
105 44 72 104 3jca ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( ∪ 𝑇 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ) )
106 rabexg ⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ V )
107 issiga ⊢ ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ V → ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝑇 ) ↔ ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝒫 ∪ 𝑇 ∧ ( ∪ 𝑇 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ) ) ) )
108 6 106 107 3syl ⊢ ( 𝜑 → ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝑇 ) ↔ ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝒫 ∪ 𝑇 ∧ ( ∪ 𝑇 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ) ) ) )
109 108 biimpar ⊢ ( ( 𝜑 ∧ ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝒫 ∪ 𝑇 ∧ ( ∪ 𝑇 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( ∪ 𝑇 ∖ 𝑥 ) ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∧ ∀ 𝑥 ∈ 𝒫 { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ( 𝑥 ≼ ω → ∪ 𝑥 ∈ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) ) ) ) → { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝑇 ) )
110 33 37 105 109 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝑇 ) )
111 3 unieqd ⊢ ( 𝜑 → ∪ 𝑇 = ∪ ( sigaGen ‘ 𝐾 ) )
112 unisg ⊢ ( 𝐾 ∈ V → ∪ ( sigaGen ‘ 𝐾 ) = ∪ 𝐾 )
113 1 112 syl ⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐾 ) = ∪ 𝐾 )
114 111 113 eqtrd ⊢ ( 𝜑 → ∪ 𝑇 = ∪ 𝐾 )
115 114 fveq2d ⊢ ( 𝜑 → ( sigAlgebra ‘ ∪ 𝑇 ) = ( sigAlgebra ‘ ∪ 𝐾 ) )
116 115 eleq2d ⊢ ( 𝜑 → ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝑇 ) ↔ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝐾 ) ) )
117 116 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝑇 ) ↔ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝐾 ) ) )
118 110 117 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝐾 ) )
119 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝐾 ⊆ 𝑇 )
120 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
121 ssrab ⊢ ( 𝐾 ⊆ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ( 𝐾 ⊆ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) )
122 119 120 121 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝐾 ⊆ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
123 sigagenss ⊢ ( ( { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ∈ ( sigAlgebra ‘ ∪ 𝐾 ) ∧ 𝐾 ⊆ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ) → ( sigaGen ‘ 𝐾 ) ⊆ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
124 118 122 123 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( sigaGen ‘ 𝐾 ) ⊆ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
125 32 124 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝑇 ⊆ { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
126 34 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ⊆ 𝑇 )
127 125 126 eqssd ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝑇 = { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } )
128 rabid2 ⊢ ( 𝑇 = { 𝑎 ∈ 𝑇 ∣ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 } ↔ ∀ 𝑎 ∈ 𝑇 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
129 127 128 sylib ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ∀ 𝑎 ∈ 𝑇 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
130 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
131 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝑇 ∈ ∪ ran sigAlgebra )
132 130 131 ismbfm ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑎 ∈ 𝑇 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) )
133 31 129 132 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
134 21 133 impbida ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) )