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	$⊢ φ \to K \in V$
	imambfm.2	$⊢ φ \to S \in ⋃ ran sigAlgebra$
	imambfm.3	$⊢ φ \to T = 𝛔 (K)$
Assertion	imambfm	$⊢ φ \to (F \in (S {MblFn}_{μ} T) \leftrightarrow (F : ⋃ S ⟶ ⋃ T \land \forall a \in K F^{-1} [a] \in S))$

Proof

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

Metamath Proof Explorer

Theorem imambfm

Proof