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 32862
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 481 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑆 ran sigAlgebra)
3 imambfm.3 . . . . . 6 (𝜑𝑇 = (sigaGen‘𝐾))
4 imambfm.1 . . . . . . 7 (𝜑𝐾 ∈ V)
54sgsiga 32741 . . . . . 6 (𝜑 → (sigaGen‘𝐾) ∈ ran sigAlgebra)
63, 5eqeltrd 2838 . . . . 5 (𝜑𝑇 ran sigAlgebra)
76adantr 481 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑇 ran sigAlgebra)
8 simpr 485 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹 ∈ (𝑆MblFnM𝑇))
92, 7, 8mbfmf 32853 . . 3 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹: 𝑆 𝑇)
101ad2antrr 724 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑆 ran sigAlgebra)
116ad2antrr 724 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑇 ran sigAlgebra)
12 simplr 767 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝐹 ∈ (𝑆MblFnM𝑇))
13 sssigagen 32744 . . . . . . . . 9 (𝐾 ∈ V → 𝐾 ⊆ (sigaGen‘𝐾))
144, 13syl 17 . . . . . . . 8 (𝜑𝐾 ⊆ (sigaGen‘𝐾))
1514, 3sseqtrrd 3985 . . . . . . 7 (𝜑𝐾𝑇)
1615ad2antrr 724 . . . . . 6 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝐾𝑇)
17 simpr 485 . . . . . 6 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑎𝐾)
1816, 17sseldd 3945 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑎𝑇)
1910, 11, 12, 18mbfmcnvima 32855 . . . 4 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → (𝐹𝑎) ∈ 𝑆)
2019ralrimiva 3143 . . 3 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)
219, 20jca 512 . 2 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
22 unielsiga 32727 . . . . . 6 (𝑇 ran sigAlgebra → 𝑇𝑇)
236, 22syl 17 . . . . 5 (𝜑 𝑇𝑇)
2423adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇𝑇)
25 unielsiga 32727 . . . . . 6 (𝑆 ran sigAlgebra → 𝑆𝑆)
261, 25syl 17 . . . . 5 (𝜑 𝑆𝑆)
2726adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑆𝑆)
28 simprl 769 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹: 𝑆 𝑇)
29 elmapg 8778 . . . . 5 (( 𝑇𝑇 𝑆𝑆) → (𝐹 ∈ ( 𝑇m 𝑆) ↔ 𝐹: 𝑆 𝑇))
3029biimpar 478 . . . 4 ((( 𝑇𝑇 𝑆𝑆) ∧ 𝐹: 𝑆 𝑇) → 𝐹 ∈ ( 𝑇m 𝑆))
3124, 27, 28, 30syl21anc 836 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹 ∈ ( 𝑇m 𝑆))
323adantr 481 . . . . . 6 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 = (sigaGen‘𝐾))
33 simpl 483 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝜑)
34 ssrab2 4037 . . . . . . . . . . 11 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇
35 pwuni 4906 . . . . . . . . . . 11 𝑇 ⊆ 𝒫 𝑇
3634, 35sstri 3953 . . . . . . . . . 10 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
3736a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇)
38 fimacnv 6690 . . . . . . . . . . . . 13 (𝐹: 𝑆 𝑇 → (𝐹 𝑇) = 𝑆)
3938ad2antrl 726 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 𝑇) = 𝑆)
4039, 27eqeltrd 2838 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 𝑇) ∈ 𝑆)
41 imaeq2 6009 . . . . . . . . . . . . 13 (𝑎 = 𝑇 → (𝐹𝑎) = (𝐹 𝑇))
4241eleq1d 2822 . . . . . . . . . . . 12 (𝑎 = 𝑇 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 𝑇) ∈ 𝑆))
4342elrab 3645 . . . . . . . . . . 11 ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ( 𝑇𝑇 ∧ (𝐹 𝑇) ∈ 𝑆))
4424, 40, 43sylanbrc 583 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
456ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑇 ran sigAlgebra)
4645, 22syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑇𝑇)
47 elrabi 3639 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → 𝑥𝑇)
4847adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑥𝑇)
49 difelsiga 32732 . . . . . . . . . . . . 13 ((𝑇 ran sigAlgebra ∧ 𝑇𝑇𝑥𝑇) → ( 𝑇𝑥) ∈ 𝑇)
5045, 46, 48, 49syl3anc 1371 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑇𝑥) ∈ 𝑇)
51 simplrl 775 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝐹: 𝑆 𝑇)
52 ffun 6671 . . . . . . . . . . . . . 14 (𝐹: 𝑆 𝑇 → Fun 𝐹)
53 difpreima 7015 . . . . . . . . . . . . . 14 (Fun 𝐹 → (𝐹 “ ( 𝑇𝑥)) = ((𝐹 𝑇) ∖ (𝐹𝑥)))
5451, 52, 533syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹 “ ( 𝑇𝑥)) = ((𝐹 𝑇) ∖ (𝐹𝑥)))
5539difeq1d 4081 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ((𝐹 𝑇) ∖ (𝐹𝑥)) = ( 𝑆 ∖ (𝐹𝑥)))
5655adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ((𝐹 𝑇) ∖ (𝐹𝑥)) = ( 𝑆 ∖ (𝐹𝑥)))
571ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑆 ran sigAlgebra)
5857, 25syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑆𝑆)
59 imaeq2 6009 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
6059eleq1d 2822 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑥 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹𝑥) ∈ 𝑆))
6160elrab 3645 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝑥𝑇 ∧ (𝐹𝑥) ∈ 𝑆))
6261simprbi 497 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → (𝐹𝑥) ∈ 𝑆)
6362adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹𝑥) ∈ 𝑆)
64 difelsiga 32732 . . . . . . . . . . . . . . 15 ((𝑆 ran sigAlgebra ∧ 𝑆𝑆 ∧ (𝐹𝑥) ∈ 𝑆) → ( 𝑆 ∖ (𝐹𝑥)) ∈ 𝑆)
6557, 58, 63, 64syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑆 ∖ (𝐹𝑥)) ∈ 𝑆)
6656, 65eqeltrd 2838 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ((𝐹 𝑇) ∖ (𝐹𝑥)) ∈ 𝑆)
6754, 66eqeltrd 2838 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆)
68 imaeq2 6009 . . . . . . . . . . . . . 14 (𝑎 = ( 𝑇𝑥) → (𝐹𝑎) = (𝐹 “ ( 𝑇𝑥)))
6968eleq1d 2822 . . . . . . . . . . . . 13 (𝑎 = ( 𝑇𝑥) → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆))
7069elrab 3645 . . . . . . . . . . . 12 (( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (( 𝑇𝑥) ∈ 𝑇 ∧ (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆))
7150, 67, 70sylanbrc 583 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
7271ralrimiva 3143 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
736ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑇 ran sigAlgebra)
7434sspwi 4572 . . . . . . . . . . . . . . . 16 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
7574sseli 3940 . . . . . . . . . . . . . . 15 (𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → 𝑥 ∈ 𝒫 𝑇)
7675ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝑇)
77 simpr 485 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
78 sigaclcu 32716 . . . . . . . . . . . . . 14 ((𝑇 ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇𝑥 ≼ ω) → 𝑥𝑇)
7973, 76, 77, 78syl3anc 1371 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥𝑇)
80 simpllr 774 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
8180simpld 495 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝐹: 𝑆 𝑇)
82 unipreima 31560 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 𝑥) = 𝑦𝑥 (𝐹𝑦))
8381, 52, 823syl 18 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹 𝑥) = 𝑦𝑥 (𝐹𝑦))
841ad3antrrr 728 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑆 ran sigAlgebra)
85 simpr 485 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑦𝑥)
86 simpllr 774 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
87 elelpwi 4570 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑥𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
8885, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
89 imaeq2 6009 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑦 → (𝐹𝑎) = (𝐹𝑦))
9089eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑦 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹𝑦) ∈ 𝑆))
9190elrab 3645 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝑦𝑇 ∧ (𝐹𝑦) ∈ 𝑆))
9291simprbi 497 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → (𝐹𝑦) ∈ 𝑆)
9388, 92syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ 𝑆)
9493ralrimiva 3143 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∀𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
95 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑦𝑥
9695sigaclcuni 32717 . . . . . . . . . . . . . . 15 ((𝑆 ran sigAlgebra ∧ ∀𝑦𝑥 (𝐹𝑦) ∈ 𝑆𝑥 ≼ ω) → 𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
9784, 94, 77, 96syl3anc 1371 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
9883, 97eqeltrd 2838 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹 𝑥) ∈ 𝑆)
99 imaeq2 6009 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹 𝑥))
10099eleq1d 2822 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 𝑥) ∈ 𝑆))
101100elrab 3645 . . . . . . . . . . . . 13 ( 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ( 𝑥𝑇 ∧ (𝐹 𝑥) ∈ 𝑆))
10279, 98, 101sylanbrc 583 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
103102ex 413 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}))
104103ralrimiva 3143 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}))
10544, 72, 1043jca 1128 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))
106 rabexg 5288 . . . . . . . . . . 11 (𝑇 ran sigAlgebra → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ V)
107 issiga 32711 . . . . . . . . . . 11 ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ V → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))))
1086, 106, 1073syl 18 . . . . . . . . . 10 (𝜑 → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))))
109108biimpar 478 . . . . . . . . 9 ((𝜑 ∧ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇))
11033, 37, 105, 109syl12anc 835 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇))
1113unieqd 4879 . . . . . . . . . . . 12 (𝜑 𝑇 = (sigaGen‘𝐾))
112 unisg 32742 . . . . . . . . . . . . 13 (𝐾 ∈ V → (sigaGen‘𝐾) = 𝐾)
1134, 112syl 17 . . . . . . . . . . . 12 (𝜑 (sigaGen‘𝐾) = 𝐾)
114111, 113eqtrd 2776 . . . . . . . . . . 11 (𝜑 𝑇 = 𝐾)
115114fveq2d 6846 . . . . . . . . . 10 (𝜑 → (sigAlgebra‘ 𝑇) = (sigAlgebra‘ 𝐾))
116115eleq2d 2823 . . . . . . . . 9 (𝜑 → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾)))
117116adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾)))
118110, 117mpbid 231 . . . . . . 7 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾))
11915adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐾𝑇)
120 simprr 771 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)
121 ssrab 4030 . . . . . . . 8 (𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝐾𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
122119, 120, 121sylanbrc 583 . . . . . . 7 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
123 sigagenss 32748 . . . . . . 7 (({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾) ∧ 𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (sigaGen‘𝐾) ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
124118, 122, 123syl2anc 584 . . . . . 6 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (sigaGen‘𝐾) ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
12532, 124eqsstrd 3982 . . . . 5 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
12634a1i 11 . . . . 5 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇)
127125, 126eqssd 3961 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 = {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
128 rabid2 3436 . . . 4 (𝑇 = {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)
129127, 128sylib 217 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)
1301adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑆 ran sigAlgebra)
1316adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ran sigAlgebra)
132130, 131ismbfm 32850 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ ( 𝑇m 𝑆) ∧ ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)))
13331, 129, 132mpbir2and 711 . 2 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹 ∈ (𝑆MblFnM𝑇))
13421, 133impbida 799 1 (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  {crab 3407  Vcvv 3445  cdif 3907  wss 3910  𝒫 cpw 4560   cuni 4865   ciun 4954   class class class wbr 5105  ccnv 5632  ran crn 5634  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  ωcom 7802  m cmap 8765  cdom 8881  sigAlgebracsiga 32707  sigaGencsigagen 32737  MblFnMcmbfm 32848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-ac2 10399
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-dju 9837  df-card 9875  df-acn 9878  df-ac 10052  df-siga 32708  df-sigagen 32738  df-mbfm 32849
This theorem is referenced by:  cnmbfm  32863  mbfmco2  32865
  Copyright terms: Public domain W3C validator