imambfm - Mathbox for Thierry Arnoux

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

Theorem imambfm 29651

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.

Step	Hyp	Ref	Expression
1		imambfm.2	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
2	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑆 ∈ ∪ ran sigAlgebra)
3		imambfm.3	. . . . . 6 ⊢ (𝜑 → 𝑇 = (sigaGen‘𝐾))
4		imambfm.1	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ V)
5	4	sgsiga 29532	. . . . . 6 ⊢ (𝜑 → (sigaGen‘𝐾) ∈ ∪ ran sigAlgebra)
6	3, 5	eqeltrd 2688	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)
7	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑇 ∈ ∪ ran sigAlgebra)
8		simpr 476	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹 ∈ (𝑆MblFnM𝑇))
9	2, 7, 8	mbfmf 29644	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹:∪ 𝑆⟶∪ 𝑇)
10	1	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑆 ∈ ∪ ran sigAlgebra)
11	6	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑇 ∈ ∪ ran sigAlgebra)
12		simplr 788	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝐹 ∈ (𝑆MblFnM𝑇))
13		sssigagen 29535	. . . . . . . . 9 ⊢ (𝐾 ∈ V → 𝐾 ⊆ (sigaGen‘𝐾))
14	4, 13	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ⊆ (sigaGen‘𝐾))
15	14, 3	sseqtr4d 3605	. . . . . . 7 ⊢ (𝜑 → 𝐾 ⊆ 𝑇)
16	15	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝐾 ⊆ 𝑇)
17		simpr 476	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾)
18	16, 17	sseldd 3569	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝑇)
19	10, 11, 12, 18	mbfmcnvima 29646	. . . 4 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → (^◡𝐹 “ 𝑎) ∈ 𝑆)
20	19	ralrimiva 2949	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)
21	9, 20	jca 553	. 2 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆))
22		unielsiga 29518	. . . . . 6 ⊢ (𝑇 ∈ ∪ ran sigAlgebra → ∪ 𝑇 ∈ 𝑇)
23	6, 22	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑇)
24	23	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∪ 𝑇 ∈ 𝑇)
25		unielsiga 29518	. . . . . 6 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
26	1, 25	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
27	26	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∪ 𝑆 ∈ 𝑆)
28		simprl 790	. . . 4 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐹:∪ 𝑆⟶∪ 𝑇)
29		elmapg 7757	. . . . 5 ⊢ ((∪ 𝑇 ∈ 𝑇 ∧ ∪ 𝑆 ∈ 𝑆) → (𝐹 ∈ (∪ 𝑇 ↑_𝑚 ∪ 𝑆) ↔ 𝐹:∪ 𝑆⟶∪ 𝑇))
30	29	biimpar 501	. . . 4 ⊢ (((∪ 𝑇 ∈ 𝑇 ∧ ∪ 𝑆 ∈ 𝑆) ∧ 𝐹:∪ 𝑆⟶∪ 𝑇) → 𝐹 ∈ (∪ 𝑇 ↑_𝑚 ∪ 𝑆))
31	24, 27, 28, 30	syl21anc 1317	. . 3 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐹 ∈ (∪ 𝑇 ↑_𝑚 ∪ 𝑆))
32	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 = (sigaGen‘𝐾))
33		simpl 472	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝜑)
34		ssrab2 3650	. . . . . . . . . . 11 ⊢ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝑇
35		pwuni 4825	. . . . . . . . . . 11 ⊢ 𝑇 ⊆ 𝒫 ∪ 𝑇
36	34, 35	sstri 3577	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇
37	36	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇)
38		fimacnv 6255	. . . . . . . . . . . . 13 ⊢ (𝐹:∪ 𝑆⟶∪ 𝑇 → (^◡𝐹 “ ∪ 𝑇) = ∪ 𝑆)
39	38	ad2antrl 760	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → (^◡𝐹 “ ∪ 𝑇) = ∪ 𝑆)
40	39, 27	eqeltrd 2688	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → (^◡𝐹 “ ∪ 𝑇) ∈ 𝑆)
41		imaeq2 5381	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∪ 𝑇 → (^◡𝐹 “ 𝑎) = (^◡𝐹 “ ∪ 𝑇))
42	41	eleq1d 2672	. . . . . . . . . . . 12 ⊢ (𝑎 = ∪ 𝑇 → ((^◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (^◡𝐹 “ ∪ 𝑇) ∈ 𝑆))
43	42	elrab 3331	. . . . . . . . . . 11 ⊢ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (∪ 𝑇 ∈ 𝑇 ∧ (^◡𝐹 “ ∪ 𝑇) ∈ 𝑆))
44	24, 40, 43	sylanbrc 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
45	6	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑇 ∈ ∪ ran sigAlgebra)
46	45, 22	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → ∪ 𝑇 ∈ 𝑇)
47		elrabi 3328	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} → 𝑥 ∈ 𝑇)
48	47	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑥 ∈ 𝑇)
49		difelsiga 29523	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 ∈ 𝑇 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) ∈ 𝑇)
50	45, 46, 48, 49	syl3anc 1318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (∪ 𝑇 ∖ 𝑥) ∈ 𝑇)
51		simplrl 796	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝐹:∪ 𝑆⟶∪ 𝑇)
52		ffun 5961	. . . . . . . . . . . . . 14 ⊢ (𝐹:∪ 𝑆⟶∪ 𝑇 → Fun 𝐹)
53		difpreima 6251	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐹 → (^◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) = ((^◡𝐹 “ ∪ 𝑇) ∖ (^◡𝐹 “ 𝑥)))
54	51, 52, 53	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (^◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) = ((^◡𝐹 “ ∪ 𝑇) ∖ (^◡𝐹 “ 𝑥)))
55	39	difeq1d 3689	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ((^◡𝐹 “ ∪ 𝑇) ∖ (^◡𝐹 “ 𝑥)) = (∪ 𝑆 ∖ (^◡𝐹 “ 𝑥)))
56	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → ((^◡𝐹 “ ∪ 𝑇) ∖ (^◡𝐹 “ 𝑥)) = (∪ 𝑆 ∖ (^◡𝐹 “ 𝑥)))
57	1	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑆 ∈ ∪ ran sigAlgebra)
58	57, 25	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → ∪ 𝑆 ∈ 𝑆)
59		imaeq2 5381	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑥 → (^◡𝐹 “ 𝑎) = (^◡𝐹 “ 𝑥))
60	59	eleq1d 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑥 → ((^◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (^◡𝐹 “ 𝑥) ∈ 𝑆))
61	60	elrab 3331	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (𝑥 ∈ 𝑇 ∧ (^◡𝐹 “ 𝑥) ∈ 𝑆))
62	61	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} → (^◡𝐹 “ 𝑥) ∈ 𝑆)
63	62	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (^◡𝐹 “ 𝑥) ∈ 𝑆)
64		difelsiga 29523	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑆 ∈ 𝑆 ∧ (^◡𝐹 “ 𝑥) ∈ 𝑆) → (∪ 𝑆 ∖ (^◡𝐹 “ 𝑥)) ∈ 𝑆)
65	57, 58, 63, 64	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (∪ 𝑆 ∖ (^◡𝐹 “ 𝑥)) ∈ 𝑆)
66	56, 65	eqeltrd 2688	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → ((^◡𝐹 “ ∪ 𝑇) ∖ (^◡𝐹 “ 𝑥)) ∈ 𝑆)
67	54, 66	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (^◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) ∈ 𝑆)
68		imaeq2 5381	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (∪ 𝑇 ∖ 𝑥) → (^◡𝐹 “ 𝑎) = (^◡𝐹 “ (∪ 𝑇 ∖ 𝑥)))
69	68	eleq1d 2672	. . . . . . . . . . . . 13 ⊢ (𝑎 = (∪ 𝑇 ∖ 𝑥) → ((^◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (^◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) ∈ 𝑆))
70	69	elrab 3331	. . . . . . . . . . . 12 ⊢ ((∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ ((∪ 𝑇 ∖ 𝑥) ∈ 𝑇 ∧ (^◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) ∈ 𝑆))
71	50, 67, 70	sylanbrc 695	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
72	71	ralrimiva 2949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
73	6	ad3antrrr 762	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑇 ∈ ∪ ran sigAlgebra)
74		sspwb 4844	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝑇 ↔ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇)
75	34, 74	mpbi 219	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇
76	75	sseli 3564	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} → 𝑥 ∈ 𝒫 𝑇)
77	76	ad2antlr 759	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝑇)
78		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
79		sigaclcu 29507	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇 ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ 𝑇)
80	73, 77, 78, 79	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ 𝑇)
81		simpllr 795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆))
82	81	simpld 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝐹:∪ 𝑆⟶∪ 𝑇)
83		unipreima 28826	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝐹 → (^◡𝐹 “ ∪ 𝑥) = ∪ 𝑦 ∈ 𝑥 (^◡𝐹 “ 𝑦))
84	82, 52, 83	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (^◡𝐹 “ ∪ 𝑥) = ∪ 𝑦 ∈ 𝑥 (^◡𝐹 “ 𝑦))
85	1	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑆 ∈ ∪ ran sigAlgebra)
86		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
87		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
88		elelpwi 4119	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
89	86, 87, 88	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
90		imaeq2 5381	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑦 → (^◡𝐹 “ 𝑎) = (^◡𝐹 “ 𝑦))
91	90	eleq1d 2672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑦 → ((^◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (^◡𝐹 “ 𝑦) ∈ 𝑆))
92	91	elrab 3331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (𝑦 ∈ 𝑇 ∧ (^◡𝐹 “ 𝑦) ∈ 𝑆))
93	92	simprbi 479	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} → (^◡𝐹 “ 𝑦) ∈ 𝑆)
94	89, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → (^◡𝐹 “ 𝑦) ∈ 𝑆)
95	94	ralrimiva 2949	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∀𝑦 ∈ 𝑥 (^◡𝐹 “ 𝑦) ∈ 𝑆)
96		nfcv 2751	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦𝑥
97	96	sigaclcuni 29508	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑦 ∈ 𝑥 (^◡𝐹 “ 𝑦) ∈ 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑦 ∈ 𝑥 (^◡𝐹 “ 𝑦) ∈ 𝑆)
98	85, 95, 78, 97	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∪ 𝑦 ∈ 𝑥 (^◡𝐹 “ 𝑦) ∈ 𝑆)
99	84, 98	eqeltrd 2688	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (^◡𝐹 “ ∪ 𝑥) ∈ 𝑆)
100		imaeq2 5381	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ∪ 𝑥 → (^◡𝐹 “ 𝑎) = (^◡𝐹 “ ∪ 𝑥))
101	100	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ∪ 𝑥 → ((^◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (^◡𝐹 “ ∪ 𝑥) ∈ 𝑆))
102	101	elrab 3331	. . . . . . . . . . . . 13 ⊢ (∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (∪ 𝑥 ∈ 𝑇 ∧ (^◡𝐹 “ ∪ 𝑥) ∈ 𝑆))
103	80, 99, 102	sylanbrc 695	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
104	103	ex 449	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (𝑥 ≼ ω → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}))
105	104	ralrimiva 2949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}))
106	44, 72, 105	3jca 1235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})))
107		rabexg 4739	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ∪ ran sigAlgebra → {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ V)
108		issiga 29501	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ V → ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇) ↔ ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇 ∧ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})))))
109	6, 107, 108	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇) ↔ ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇 ∧ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})))))
110	109	biimpar 501	. . . . . . . . 9 ⊢ ((𝜑 ∧ ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇 ∧ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})))) → {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇))
111	33, 37, 106, 110	syl12anc 1316	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇))
112	3	unieqd 4382	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑇 = ∪ (sigaGen‘𝐾))
113		unisg 29533	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ V → ∪ (sigaGen‘𝐾) = ∪ 𝐾)
114	4, 113	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (sigaGen‘𝐾) = ∪ 𝐾)
115	112, 114	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑇 = ∪ 𝐾)
116	115	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (sigAlgebra‘∪ 𝑇) = (sigAlgebra‘∪ 𝐾))
117	116	eleq2d 2673	. . . . . . . . 9 ⊢ (𝜑 → ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇) ↔ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾)))
118	117	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇) ↔ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾)))
119	111, 118	mpbid 221	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾))
120	15	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐾 ⊆ 𝑇)
121		simprr 792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)
122		ssrab 3643	. . . . . . . 8 ⊢ (𝐾 ⊆ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (𝐾 ⊆ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆))
123	120, 121, 122	sylanbrc 695	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐾 ⊆ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
124		sigagenss 29539	. . . . . . 7 ⊢ (({𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾) ∧ 𝐾 ⊆ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆}) → (sigaGen‘𝐾) ⊆ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
125	119, 123, 124	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → (sigaGen‘𝐾) ⊆ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
126	32, 125	eqsstrd 3602	. . . . 5 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 ⊆ {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
127	34	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝑇)
128	126, 127	eqssd 3585	. . . 4 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 = {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆})
129		rabid2 3096	. . . 4 ⊢ (𝑇 = {𝑎 ∈ 𝑇 ∣ (^◡𝐹 “ 𝑎) ∈ 𝑆} ↔ ∀𝑎 ∈ 𝑇 (^◡𝐹 “ 𝑎) ∈ 𝑆)
130	128, 129	sylib 207	. . 3 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑎 ∈ 𝑇 (^◡𝐹 “ 𝑎) ∈ 𝑆)
131	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑆 ∈ ∪ ran sigAlgebra)
132	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 ∈ ∪ ran sigAlgebra)
133	131, 132	ismbfm 29641	. . 3 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ (∪ 𝑇 ↑_𝑚 ∪ 𝑆) ∧ ∀𝑎 ∈ 𝑇 (^◡𝐹 “ 𝑎) ∈ 𝑆)))
134	31, 130, 133	mpbir2and 959	. 2 ⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐹 ∈ (𝑆MblFnM𝑇))
135	21, 134	impbida 873	1 ⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (^◡𝐹 “ 𝑎) ∈ 𝑆)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 {crab 2900 Vcvv 3173 ∖ cdif 3537 ⊆ wss 3540 𝒫 cpw 4108 ∪ cuni 4372 ∪ ciun 4455 class class class wbr 4583 ^◡ccnv 5037 ran crn 5039 “ cima 5041 Fun wfun 5798 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ωcom 6957 ↑_𝑚 cmap 7744 ≼ cdom 7839 sigAlgebracsiga 29497 sigaGencsigagen 29528 MblFnMcmbfm 29639

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-ac2 9168

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-oi 8298 df-card 8648 df-acn 8651 df-ac 8822 df-cda 8873 df-siga 29498 df-sigagen 29529 df-mbfm 29640

This theorem is referenced by: cnmbfm 29652 mbfmco2 29654

W3C validator