Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  imambfm Structured version   Visualization version   GIF version

Theorem imambfm 30705
Description: If the sigma-algebra in the range of a given function is generated by a collection of basic sets 𝐾, then to check the measurability of that function, we need only consider inverse images of basic sets 𝑎. (Contributed by Thierry Arnoux, 4-Jun-2017.)
Hypotheses
Ref Expression
imambfm.1 (𝜑𝐾 ∈ V)
imambfm.2 (𝜑𝑆 ran sigAlgebra)
imambfm.3 (𝜑𝑇 = (sigaGen‘𝐾))
Assertion
Ref Expression
imambfm (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)))
Distinct variable groups:   𝐹,𝑎   𝐾,𝑎   𝑆,𝑎   𝑇,𝑎   𝜑,𝑎

Proof of Theorem imambfm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imambfm.2 . . . . 5 (𝜑𝑆 ran sigAlgebra)
21adantr 472 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑆 ran sigAlgebra)
3 imambfm.3 . . . . . 6 (𝜑𝑇 = (sigaGen‘𝐾))
4 imambfm.1 . . . . . . 7 (𝜑𝐾 ∈ V)
54sgsiga 30586 . . . . . 6 (𝜑 → (sigaGen‘𝐾) ∈ ran sigAlgebra)
63, 5eqeltrd 2843 . . . . 5 (𝜑𝑇 ran sigAlgebra)
76adantr 472 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑇 ran sigAlgebra)
8 simpr 477 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹 ∈ (𝑆MblFnM𝑇))
92, 7, 8mbfmf 30698 . . 3 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹: 𝑆 𝑇)
101ad2antrr 717 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑆 ran sigAlgebra)
116ad2antrr 717 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑇 ran sigAlgebra)
12 simplr 785 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝐹 ∈ (𝑆MblFnM𝑇))
13 sssigagen 30589 . . . . . . . . 9 (𝐾 ∈ V → 𝐾 ⊆ (sigaGen‘𝐾))
144, 13syl 17 . . . . . . . 8 (𝜑𝐾 ⊆ (sigaGen‘𝐾))
1514, 3sseqtr4d 3801 . . . . . . 7 (𝜑𝐾𝑇)
1615ad2antrr 717 . . . . . 6 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝐾𝑇)
17 simpr 477 . . . . . 6 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑎𝐾)
1816, 17sseldd 3761 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑎𝑇)
1910, 11, 12, 18mbfmcnvima 30700 . . . 4 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → (𝐹𝑎) ∈ 𝑆)
2019ralrimiva 3112 . . 3 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)
219, 20jca 507 . 2 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
22 unielsiga 30572 . . . . . 6 (𝑇 ran sigAlgebra → 𝑇𝑇)
236, 22syl 17 . . . . 5 (𝜑 𝑇𝑇)
2423adantr 472 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇𝑇)
25 unielsiga 30572 . . . . . 6 (𝑆 ran sigAlgebra → 𝑆𝑆)
261, 25syl 17 . . . . 5 (𝜑 𝑆𝑆)
2726adantr 472 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑆𝑆)
28 simprl 787 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹: 𝑆 𝑇)
29 elmapg 8072 . . . . 5 (( 𝑇𝑇 𝑆𝑆) → (𝐹 ∈ ( 𝑇𝑚 𝑆) ↔ 𝐹: 𝑆 𝑇))
3029biimpar 469 . . . 4 ((( 𝑇𝑇 𝑆𝑆) ∧ 𝐹: 𝑆 𝑇) → 𝐹 ∈ ( 𝑇𝑚 𝑆))
3124, 27, 28, 30syl21anc 866 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹 ∈ ( 𝑇𝑚 𝑆))
323adantr 472 . . . . . 6 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 = (sigaGen‘𝐾))
33 simpl 474 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝜑)
34 ssrab2 3846 . . . . . . . . . . 11 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇
35 pwuni 4631 . . . . . . . . . . 11 𝑇 ⊆ 𝒫 𝑇
3634, 35sstri 3769 . . . . . . . . . 10 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
3736a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇)
38 fimacnv 6536 . . . . . . . . . . . . 13 (𝐹: 𝑆 𝑇 → (𝐹 𝑇) = 𝑆)
3938ad2antrl 719 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 𝑇) = 𝑆)
4039, 27eqeltrd 2843 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 𝑇) ∈ 𝑆)
41 imaeq2 5643 . . . . . . . . . . . . 13 (𝑎 = 𝑇 → (𝐹𝑎) = (𝐹 𝑇))
4241eleq1d 2828 . . . . . . . . . . . 12 (𝑎 = 𝑇 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 𝑇) ∈ 𝑆))
4342elrab 3518 . . . . . . . . . . 11 ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ( 𝑇𝑇 ∧ (𝐹 𝑇) ∈ 𝑆))
4424, 40, 43sylanbrc 578 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
456ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑇 ran sigAlgebra)
4645, 22syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑇𝑇)
47 elrabi 3513 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → 𝑥𝑇)
4847adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑥𝑇)
49 difelsiga 30577 . . . . . . . . . . . . 13 ((𝑇 ran sigAlgebra ∧ 𝑇𝑇𝑥𝑇) → ( 𝑇𝑥) ∈ 𝑇)
5045, 46, 48, 49syl3anc 1490 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑇𝑥) ∈ 𝑇)
51 simplrl 795 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝐹: 𝑆 𝑇)
52 ffun 6225 . . . . . . . . . . . . . 14 (𝐹: 𝑆 𝑇 → Fun 𝐹)
53 difpreima 6532 . . . . . . . . . . . . . 14 (Fun 𝐹 → (𝐹 “ ( 𝑇𝑥)) = ((𝐹 𝑇) ∖ (𝐹𝑥)))
5451, 52, 533syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹 “ ( 𝑇𝑥)) = ((𝐹 𝑇) ∖ (𝐹𝑥)))
5539difeq1d 3888 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ((𝐹 𝑇) ∖ (𝐹𝑥)) = ( 𝑆 ∖ (𝐹𝑥)))
5655adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ((𝐹 𝑇) ∖ (𝐹𝑥)) = ( 𝑆 ∖ (𝐹𝑥)))
571ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑆 ran sigAlgebra)
5857, 25syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑆𝑆)
59 imaeq2 5643 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
6059eleq1d 2828 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑥 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹𝑥) ∈ 𝑆))
6160elrab 3518 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝑥𝑇 ∧ (𝐹𝑥) ∈ 𝑆))
6261simprbi 490 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → (𝐹𝑥) ∈ 𝑆)
6362adantl 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹𝑥) ∈ 𝑆)
64 difelsiga 30577 . . . . . . . . . . . . . . 15 ((𝑆 ran sigAlgebra ∧ 𝑆𝑆 ∧ (𝐹𝑥) ∈ 𝑆) → ( 𝑆 ∖ (𝐹𝑥)) ∈ 𝑆)
6557, 58, 63, 64syl3anc 1490 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑆 ∖ (𝐹𝑥)) ∈ 𝑆)
6656, 65eqeltrd 2843 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ((𝐹 𝑇) ∖ (𝐹𝑥)) ∈ 𝑆)
6754, 66eqeltrd 2843 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆)
68 imaeq2 5643 . . . . . . . . . . . . . 14 (𝑎 = ( 𝑇𝑥) → (𝐹𝑎) = (𝐹 “ ( 𝑇𝑥)))
6968eleq1d 2828 . . . . . . . . . . . . 13 (𝑎 = ( 𝑇𝑥) → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆))
7069elrab 3518 . . . . . . . . . . . 12 (( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (( 𝑇𝑥) ∈ 𝑇 ∧ (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆))
7150, 67, 70sylanbrc 578 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
7271ralrimiva 3112 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
736ad3antrrr 721 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑇 ran sigAlgebra)
74 sspwb 5072 . . . . . . . . . . . . . . . . 17 ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇 ↔ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇)
7534, 74mpbi 221 . . . . . . . . . . . . . . . 16 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
7675sseli 3756 . . . . . . . . . . . . . . 15 (𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → 𝑥 ∈ 𝒫 𝑇)
7776ad2antlr 718 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝑇)
78 simpr 477 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
79 sigaclcu 30561 . . . . . . . . . . . . . 14 ((𝑇 ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇𝑥 ≼ ω) → 𝑥𝑇)
8073, 77, 78, 79syl3anc 1490 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥𝑇)
81 simpllr 793 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
8281simpld 488 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝐹: 𝑆 𝑇)
83 unipreima 29830 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 𝑥) = 𝑦𝑥 (𝐹𝑦))
8482, 52, 833syl 18 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹 𝑥) = 𝑦𝑥 (𝐹𝑦))
851ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑆 ran sigAlgebra)
86 simpr 477 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑦𝑥)
87 simpllr 793 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
88 elelpwi 4327 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑥𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
8986, 87, 88syl2anc 579 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
90 imaeq2 5643 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑦 → (𝐹𝑎) = (𝐹𝑦))
9190eleq1d 2828 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑦 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹𝑦) ∈ 𝑆))
9291elrab 3518 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝑦𝑇 ∧ (𝐹𝑦) ∈ 𝑆))
9392simprbi 490 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → (𝐹𝑦) ∈ 𝑆)
9489, 93syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ 𝑆)
9594ralrimiva 3112 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∀𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
96 nfcv 2906 . . . . . . . . . . . . . . . 16 𝑦𝑥
9796sigaclcuni 30562 . . . . . . . . . . . . . . 15 ((𝑆 ran sigAlgebra ∧ ∀𝑦𝑥 (𝐹𝑦) ∈ 𝑆𝑥 ≼ ω) → 𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
9885, 95, 78, 97syl3anc 1490 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
9984, 98eqeltrd 2843 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹 𝑥) ∈ 𝑆)
100 imaeq2 5643 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹 𝑥))
101100eleq1d 2828 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 𝑥) ∈ 𝑆))
102101elrab 3518 . . . . . . . . . . . . 13 ( 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ( 𝑥𝑇 ∧ (𝐹 𝑥) ∈ 𝑆))
10380, 99, 102sylanbrc 578 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
104103ex 401 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}))
105104ralrimiva 3112 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}))
10644, 72, 1053jca 1158 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))
107 rabexg 4971 . . . . . . . . . . 11 (𝑇 ran sigAlgebra → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ V)
108 issiga 30555 . . . . . . . . . . 11 ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ V → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))))
1096, 107, 1083syl 18 . . . . . . . . . 10 (𝜑 → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))))
110109biimpar 469 . . . . . . . . 9 ((𝜑 ∧ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇))
11133, 37, 106, 110syl12anc 865 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇))
1123unieqd 4603 . . . . . . . . . . . 12 (𝜑 𝑇 = (sigaGen‘𝐾))
113 unisg 30587 . . . . . . . . . . . . 13 (𝐾 ∈ V → (sigaGen‘𝐾) = 𝐾)
1144, 113syl 17 . . . . . . . . . . . 12 (𝜑 (sigaGen‘𝐾) = 𝐾)
115112, 114eqtrd 2798 . . . . . . . . . . 11 (𝜑 𝑇 = 𝐾)
116115fveq2d 6378 . . . . . . . . . 10 (𝜑 → (sigAlgebra‘ 𝑇) = (sigAlgebra‘ 𝐾))
117116eleq2d 2829 . . . . . . . . 9 (𝜑 → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾)))
118117adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾)))
119111, 118mpbid 223 . . . . . . 7 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾))
12015adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐾𝑇)
121 simprr 789 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)
122 ssrab 3839 . . . . . . . 8 (𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝐾𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
123120, 121, 122sylanbrc 578 . . . . . . 7 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
124 sigagenss 30593 . . . . . . 7 (({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾) ∧ 𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (sigaGen‘𝐾) ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
125119, 123, 124syl2anc 579 . . . . . 6 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (sigaGen‘𝐾) ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
12632, 125eqsstrd 3798 . . . . 5 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
12734a1i 11 . . . . 5 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇)
128126, 127eqssd 3777 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 = {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
129 rabid2 3265 . . . 4 (𝑇 = {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)
130128, 129sylib 209 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)
1311adantr 472 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑆 ran sigAlgebra)
1326adantr 472 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ran sigAlgebra)
133131, 132ismbfm 30695 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ ( 𝑇𝑚 𝑆) ∧ ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)))
13431, 130, 133mpbir2and 704 . 2 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹 ∈ (𝑆MblFnM𝑇))
13521, 134impbida 835 1 (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3054  {crab 3058  Vcvv 3349  cdif 3728  wss 3731  𝒫 cpw 4314   cuni 4593   ciun 4675   class class class wbr 4808  ccnv 5275  ran crn 5277  cima 5279  Fun wfun 6061  wf 6063  cfv 6067  (class class class)co 6841  ωcom 7262  𝑚 cmap 8059  cdom 8157  sigAlgebracsiga 30551  sigaGencsigagen 30582  MblFnMcmbfm 30693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-ac2 9537
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-oi 8621  df-card 9015  df-acn 9018  df-ac 9189  df-cda 9242  df-siga 30552  df-sigagen 30583  df-mbfm 30694
This theorem is referenced by:  cnmbfm  30706  mbfmco2  30708
  Copyright terms: Public domain W3C validator