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

Theorem imambfm 30102
 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 29983 . . . . . 6 (𝜑 → (sigaGen‘𝐾) ∈ ran sigAlgebra)
63, 5eqeltrd 2698 . . . . 5 (𝜑𝑇 ran sigAlgebra)
76adantr 481 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑇 ran sigAlgebra)
8 simpr 477 . . . 4 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹 ∈ (𝑆MblFnM𝑇))
92, 7, 8mbfmf 30095 . . 3 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹: 𝑆 𝑇)
101ad2antrr 761 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑆 ran sigAlgebra)
116ad2antrr 761 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑇 ran sigAlgebra)
12 simplr 791 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝐹 ∈ (𝑆MblFnM𝑇))
13 sssigagen 29986 . . . . . . . . 9 (𝐾 ∈ V → 𝐾 ⊆ (sigaGen‘𝐾))
144, 13syl 17 . . . . . . . 8 (𝜑𝐾 ⊆ (sigaGen‘𝐾))
1514, 3sseqtr4d 3621 . . . . . . 7 (𝜑𝐾𝑇)
1615ad2antrr 761 . . . . . 6 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝐾𝑇)
17 simpr 477 . . . . . 6 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑎𝐾)
1816, 17sseldd 3584 . . . . 5 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → 𝑎𝑇)
1910, 11, 12, 18mbfmcnvima 30097 . . . 4 (((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎𝐾) → (𝐹𝑎) ∈ 𝑆)
2019ralrimiva 2960 . . 3 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)
219, 20jca 554 . 2 ((𝜑𝐹 ∈ (𝑆MblFnM𝑇)) → (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
22 unielsiga 29969 . . . . . 6 (𝑇 ran sigAlgebra → 𝑇𝑇)
236, 22syl 17 . . . . 5 (𝜑 𝑇𝑇)
2423adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇𝑇)
25 unielsiga 29969 . . . . . 6 (𝑆 ran sigAlgebra → 𝑆𝑆)
261, 25syl 17 . . . . 5 (𝜑 𝑆𝑆)
2726adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑆𝑆)
28 simprl 793 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹: 𝑆 𝑇)
29 elmapg 7815 . . . . 5 (( 𝑇𝑇 𝑆𝑆) → (𝐹 ∈ ( 𝑇𝑚 𝑆) ↔ 𝐹: 𝑆 𝑇))
3029biimpar 502 . . . 4 ((( 𝑇𝑇 𝑆𝑆) ∧ 𝐹: 𝑆 𝑇) → 𝐹 ∈ ( 𝑇𝑚 𝑆))
3124, 27, 28, 30syl21anc 1322 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹 ∈ ( 𝑇𝑚 𝑆))
323adantr 481 . . . . . 6 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 = (sigaGen‘𝐾))
33 simpl 473 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝜑)
34 ssrab2 3666 . . . . . . . . . . 11 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇
35 pwuni 4859 . . . . . . . . . . 11 𝑇 ⊆ 𝒫 𝑇
3634, 35sstri 3592 . . . . . . . . . 10 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
3736a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇)
38 fimacnv 6303 . . . . . . . . . . . . 13 (𝐹: 𝑆 𝑇 → (𝐹 𝑇) = 𝑆)
3938ad2antrl 763 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 𝑇) = 𝑆)
4039, 27eqeltrd 2698 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 𝑇) ∈ 𝑆)
41 imaeq2 5421 . . . . . . . . . . . . 13 (𝑎 = 𝑇 → (𝐹𝑎) = (𝐹 𝑇))
4241eleq1d 2683 . . . . . . . . . . . 12 (𝑎 = 𝑇 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 𝑇) ∈ 𝑆))
4342elrab 3346 . . . . . . . . . . 11 ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ( 𝑇𝑇 ∧ (𝐹 𝑇) ∈ 𝑆))
4424, 40, 43sylanbrc 697 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
456ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑇 ran sigAlgebra)
4645, 22syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑇𝑇)
47 elrabi 3342 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → 𝑥𝑇)
4847adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑥𝑇)
49 difelsiga 29974 . . . . . . . . . . . . 13 ((𝑇 ran sigAlgebra ∧ 𝑇𝑇𝑥𝑇) → ( 𝑇𝑥) ∈ 𝑇)
5045, 46, 48, 49syl3anc 1323 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑇𝑥) ∈ 𝑇)
51 simplrl 799 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝐹: 𝑆 𝑇)
52 ffun 6005 . . . . . . . . . . . . . 14 (𝐹: 𝑆 𝑇 → Fun 𝐹)
53 difpreima 6299 . . . . . . . . . . . . . 14 (Fun 𝐹 → (𝐹 “ ( 𝑇𝑥)) = ((𝐹 𝑇) ∖ (𝐹𝑥)))
5451, 52, 533syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹 “ ( 𝑇𝑥)) = ((𝐹 𝑇) ∖ (𝐹𝑥)))
5539difeq1d 3705 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ((𝐹 𝑇) ∖ (𝐹𝑥)) = ( 𝑆 ∖ (𝐹𝑥)))
5655adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ((𝐹 𝑇) ∖ (𝐹𝑥)) = ( 𝑆 ∖ (𝐹𝑥)))
571ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑆 ran sigAlgebra)
5857, 25syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑆𝑆)
59 imaeq2 5421 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
6059eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑥 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹𝑥) ∈ 𝑆))
6160elrab 3346 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝑥𝑇 ∧ (𝐹𝑥) ∈ 𝑆))
6261simprbi 480 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → (𝐹𝑥) ∈ 𝑆)
6362adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹𝑥) ∈ 𝑆)
64 difelsiga 29974 . . . . . . . . . . . . . . 15 ((𝑆 ran sigAlgebra ∧ 𝑆𝑆 ∧ (𝐹𝑥) ∈ 𝑆) → ( 𝑆 ∖ (𝐹𝑥)) ∈ 𝑆)
6557, 58, 63, 64syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑆 ∖ (𝐹𝑥)) ∈ 𝑆)
6656, 65eqeltrd 2698 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ((𝐹 𝑇) ∖ (𝐹𝑥)) ∈ 𝑆)
6754, 66eqeltrd 2698 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆)
68 imaeq2 5421 . . . . . . . . . . . . . 14 (𝑎 = ( 𝑇𝑥) → (𝐹𝑎) = (𝐹 “ ( 𝑇𝑥)))
6968eleq1d 2683 . . . . . . . . . . . . 13 (𝑎 = ( 𝑇𝑥) → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆))
7069elrab 3346 . . . . . . . . . . . 12 (( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (( 𝑇𝑥) ∈ 𝑇 ∧ (𝐹 “ ( 𝑇𝑥)) ∈ 𝑆))
7150, 67, 70sylanbrc 697 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
7271ralrimiva 2960 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
736ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑇 ran sigAlgebra)
74 sspwb 4878 . . . . . . . . . . . . . . . . 17 ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇 ↔ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇)
7534, 74mpbi 220 . . . . . . . . . . . . . . . 16 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
7675sseli 3579 . . . . . . . . . . . . . . 15 (𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → 𝑥 ∈ 𝒫 𝑇)
7776ad2antlr 762 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝑇)
78 simpr 477 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
79 sigaclcu 29958 . . . . . . . . . . . . . 14 ((𝑇 ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇𝑥 ≼ ω) → 𝑥𝑇)
8073, 77, 78, 79syl3anc 1323 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥𝑇)
81 simpllr 798 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
8281simpld 475 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝐹: 𝑆 𝑇)
83 unipreima 29285 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 𝑥) = 𝑦𝑥 (𝐹𝑦))
8482, 52, 833syl 18 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹 𝑥) = 𝑦𝑥 (𝐹𝑦))
851ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑆 ran sigAlgebra)
86 simpr 477 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑦𝑥)
87 simpllr 798 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
88 elelpwi 4142 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑥𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → 𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
8986, 87, 88syl2anc 692 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → 𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
90 imaeq2 5421 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑦 → (𝐹𝑎) = (𝐹𝑦))
9190eleq1d 2683 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑦 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹𝑦) ∈ 𝑆))
9291elrab 3346 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝑦𝑇 ∧ (𝐹𝑦) ∈ 𝑆))
9392simprbi 480 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} → (𝐹𝑦) ∈ 𝑆)
9489, 93syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ 𝑆)
9594ralrimiva 2960 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∀𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
96 nfcv 2761 . . . . . . . . . . . . . . . 16 𝑦𝑥
9796sigaclcuni 29959 . . . . . . . . . . . . . . 15 ((𝑆 ran sigAlgebra ∧ ∀𝑦𝑥 (𝐹𝑦) ∈ 𝑆𝑥 ≼ ω) → 𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
9885, 95, 78, 97syl3anc 1323 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑦𝑥 (𝐹𝑦) ∈ 𝑆)
9984, 98eqeltrd 2698 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹 𝑥) ∈ 𝑆)
100 imaeq2 5421 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹 𝑥))
101100eleq1d 2683 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → ((𝐹𝑎) ∈ 𝑆 ↔ (𝐹 𝑥) ∈ 𝑆))
102101elrab 3346 . . . . . . . . . . . . 13 ( 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ( 𝑥𝑇 ∧ (𝐹 𝑥) ∈ 𝑆))
10380, 99, 102sylanbrc 697 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
104103ex 450 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}))
105104ralrimiva 2960 . . . . . . . . . 10 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}))
10644, 72, 1053jca 1240 . . . . . . . . 9 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))
107 rabexg 4772 . . . . . . . . . . 11 (𝑇 ran sigAlgebra → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ V)
108 issiga 29952 . . . . . . . . . . 11 ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ V → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))))
1096, 107, 1083syl 18 . . . . . . . . . 10 (𝜑 → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))))
110109biimpar 502 . . . . . . . . 9 ((𝜑 ∧ ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 ∧ ( 𝑇 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ( 𝑇𝑥) ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} (𝑥 ≼ ω → 𝑥 ∈ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})))) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇))
11133, 37, 106, 110syl12anc 1321 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇))
1123unieqd 4412 . . . . . . . . . . . 12 (𝜑 𝑇 = (sigaGen‘𝐾))
113 unisg 29984 . . . . . . . . . . . . 13 (𝐾 ∈ V → (sigaGen‘𝐾) = 𝐾)
1144, 113syl 17 . . . . . . . . . . . 12 (𝜑 (sigaGen‘𝐾) = 𝐾)
115112, 114eqtrd 2655 . . . . . . . . . . 11 (𝜑 𝑇 = 𝐾)
116115fveq2d 6152 . . . . . . . . . 10 (𝜑 → (sigAlgebra‘ 𝑇) = (sigAlgebra‘ 𝐾))
117116eleq2d 2684 . . . . . . . . 9 (𝜑 → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾)))
118117adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝑇) ↔ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾)))
119111, 118mpbid 222 . . . . . . 7 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾))
12015adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐾𝑇)
121 simprr 795 . . . . . . . 8 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)
122 ssrab 3659 . . . . . . . 8 (𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ (𝐾𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆))
123120, 121, 122sylanbrc 697 . . . . . . 7 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
124 sigagenss 29990 . . . . . . 7 (({𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ∈ (sigAlgebra‘ 𝐾) ∧ 𝐾 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆}) → (sigaGen‘𝐾) ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
125119, 123, 124syl2anc 692 . . . . . 6 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (sigaGen‘𝐾) ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
12632, 125eqsstrd 3618 . . . . 5 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ⊆ {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
12734a1i 11 . . . . 5 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ⊆ 𝑇)
128126, 127eqssd 3600 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 = {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆})
129 rabid2 3107 . . . 4 (𝑇 = {𝑎𝑇 ∣ (𝐹𝑎) ∈ 𝑆} ↔ ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)
130128, 129sylib 208 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)
1311adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑆 ran sigAlgebra)
1326adantr 481 . . . 4 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝑇 ran sigAlgebra)
133131, 132ismbfm 30092 . . 3 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ ( 𝑇𝑚 𝑆) ∧ ∀𝑎𝑇 (𝐹𝑎) ∈ 𝑆)))
13431, 130, 133mpbir2and 956 . 2 ((𝜑 ∧ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)) → 𝐹 ∈ (𝑆MblFnM𝑇))
13521, 134impbida 876 1 (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹: 𝑆 𝑇 ∧ ∀𝑎𝐾 (𝐹𝑎) ∈ 𝑆)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2907  {crab 2911  Vcvv 3186   ∖ cdif 3552   ⊆ wss 3555  𝒫 cpw 4130  ∪ cuni 4402  ∪ ciun 4485   class class class wbr 4613  ◡ccnv 5073  ran crn 5075   “ cima 5077  Fun wfun 5841  ⟶wf 5843  ‘cfv 5847  (class class class)co 6604  ωcom 7012   ↑𝑚 cmap 7802   ≼ cdom 7897  sigAlgebracsiga 29948  sigaGencsigagen 29979  MblFnMcmbfm 30090 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-ac2 9229 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-oi 8359  df-card 8709  df-acn 8712  df-ac 8883  df-cda 8934  df-siga 29949  df-sigagen 29980  df-mbfm 30091 This theorem is referenced by:  cnmbfm  30103  mbfmco2  30105
 Copyright terms: Public domain W3C validator