uniiccdif

Description: A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015)

		Ref	Expression
	Hypothesis	uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	Assertion	uniiccdif	$⊢ φ \to (⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F) \land {vol}^{*} (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) = 0)$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		ssun1	$⊢ ⋃ ran ((.) \circ F) \subseteq ⋃ ran ((.) \circ F) \cup (1^{st} [ran F] \cup 2^{nd} [ran F])$
3		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ \land 1^{st} (F (x)) \leq 2^{nd} (F (x)))$
4	1 3	sylan	$⊢ (φ \land x \in ℕ) \to (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ \land 1^{st} (F (x)) \leq 2^{nd} (F (x)))$
5		rexr	$⊢ 1^{st} (F (x)) \in ℝ \to 1^{st} (F (x)) \in ℝ^{*}$
6		rexr	$⊢ 2^{nd} (F (x)) \in ℝ \to 2^{nd} (F (x)) \in ℝ^{*}$
7		id	$⊢ 1^{st} (F (x)) \leq 2^{nd} (F (x)) \to 1^{st} (F (x)) \leq 2^{nd} (F (x))$
8		prunioo	$⊢ (1^{st} (F (x)) \in ℝ^{} \land 2^{nd} (F (x)) \in ℝ^{} \land 1^{st} (F (x)) \leq 2^{nd} (F (x))) \to (1^{st} (F (x)), 2^{nd} (F (x))) \cup \{1^{st} (F (x)), 2^{nd} (F (x))\} = [1^{st} (F (x)), 2^{nd} (F (x))]$
9	5 6 7 8	syl3an	$⊢ (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ \land 1^{st} (F (x)) \leq 2^{nd} (F (x))) \to (1^{st} (F (x)), 2^{nd} (F (x))) \cup \{1^{st} (F (x)), 2^{nd} (F (x))\} = [1^{st} (F (x)), 2^{nd} (F (x))]$
10	4 9	syl	$⊢ (φ \land x \in ℕ) \to (1^{st} (F (x)), 2^{nd} (F (x))) \cup \{1^{st} (F (x)), 2^{nd} (F (x))\} = [1^{st} (F (x)), 2^{nd} (F (x))]$
11		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ((.) \circ F) (x) = (.) (F (x))$
12	1 11	sylan	$⊢ (φ \land x \in ℕ) \to ((.) \circ F) (x) = (.) (F (x))$
13	1	ffvelcdmda	$⊢ (φ \land x \in ℕ) \to F (x) \in (\leq \cap ℝ^{2})$
14	13	elin2d	$⊢ (φ \land x \in ℕ) \to F (x) \in ℝ^{2}$
15		1st2nd2	$⊢ F (x) \in ℝ^{2} \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
16	14 15	syl	$⊢ (φ \land x \in ℕ) \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
17	16	fveq2d	$⊢ (φ \land x \in ℕ) \to (.) (F (x)) = (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
18		df-ov	$⊢ (1^{st} (F (x)), 2^{nd} (F (x))) = (.) (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
19	17 18	eqtr4di	$⊢ (φ \land x \in ℕ) \to (.) (F (x)) = (1^{st} (F (x)), 2^{nd} (F (x)))$
20	12 19	eqtrd	$⊢ (φ \land x \in ℕ) \to ((.) \circ F) (x) = (1^{st} (F (x)), 2^{nd} (F (x)))$
21		df-pr	$⊢ \{(1^{st} \circ F) (x), (2^{nd} \circ F) (x)\} = \{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\}$
22		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (1^{st} \circ F) (x) = 1^{st} (F (x))$
23	1 22	sylan	$⊢ (φ \land x \in ℕ) \to (1^{st} \circ F) (x) = 1^{st} (F (x))$
24		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to (2^{nd} \circ F) (x) = 2^{nd} (F (x))$
25	1 24	sylan	$⊢ (φ \land x \in ℕ) \to (2^{nd} \circ F) (x) = 2^{nd} (F (x))$
26	23 25	preq12d	$⊢ (φ \land x \in ℕ) \to \{(1^{st} \circ F) (x), (2^{nd} \circ F) (x)\} = \{1^{st} (F (x)), 2^{nd} (F (x))\}$
27	21 26	eqtr3id	$⊢ (φ \land x \in ℕ) \to \{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\} = \{1^{st} (F (x)), 2^{nd} (F (x))\}$
28	20 27	uneq12d	$⊢ (φ \land x \in ℕ) \to ((.) \circ F) (x) \cup (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\}) = (1^{st} (F (x)), 2^{nd} (F (x))) \cup \{1^{st} (F (x)), 2^{nd} (F (x))\}$
29		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land x \in ℕ) \to ([.] \circ F) (x) = [.] (F (x))$
30	1 29	sylan	$⊢ (φ \land x \in ℕ) \to ([.] \circ F) (x) = [.] (F (x))$
31	16	fveq2d	$⊢ (φ \land x \in ℕ) \to [.] (F (x)) = [.] (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
32		df-ov	$⊢ [1^{st} (F (x)), 2^{nd} (F (x))] = [.] (⟨1^{st} (F (x)), 2^{nd} (F (x))⟩)$
33	31 32	eqtr4di	$⊢ (φ \land x \in ℕ) \to [.] (F (x)) = [1^{st} (F (x)), 2^{nd} (F (x))]$
34	30 33	eqtrd	$⊢ (φ \land x \in ℕ) \to ([.] \circ F) (x) = [1^{st} (F (x)), 2^{nd} (F (x))]$
35	10 28 34	3eqtr4rd	$⊢ (φ \land x \in ℕ) \to ([.] \circ F) (x) = ((.) \circ F) (x) \cup (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\})$
36	35	iuneq2dv	$⊢ φ \to ⋃_{x \in ℕ} ([.] \circ F) (x) = ⋃_{x \in ℕ} (((.) \circ F) (x) \cup (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\}))$
37		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
38		ffn	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to [.] Fn (ℝ^{} \times ℝ^{*})$
39	37 38	ax-mp	$⊢ [.] Fn (ℝ^{} \times ℝ^{})$
40		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
41		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
42	40 41	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
43		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
44	1 42 43	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
45		fnfco	$⊢ ([.] Fn (ℝ^{} \times ℝ^{}) \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ([.] \circ F) Fn ℕ$
46	39 44 45	sylancr	$⊢ φ \to ([.] \circ F) Fn ℕ$
47		fniunfv	$⊢ ([.] \circ F) Fn ℕ \to ⋃_{x \in ℕ} ([.] \circ F) (x) = ⋃ ran ([.] \circ F)$
48	46 47	syl	$⊢ φ \to ⋃_{x \in ℕ} ([.] \circ F) (x) = ⋃ ran ([.] \circ F)$
49		iunun	$⊢ ⋃_{x \in ℕ} (((.) \circ F) (x) \cup (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\})) = ⋃_{x \in ℕ} ((.) \circ F) (x) \cup ⋃_{x \in ℕ} (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\})$
50		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
51		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
52	50 51	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
53		fnfco	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) Fn ℕ$
54	52 44 53	sylancr	$⊢ φ \to ((.) \circ F) Fn ℕ$
55		fniunfv	$⊢ ((.) \circ F) Fn ℕ \to ⋃_{x \in ℕ} ((.) \circ F) (x) = ⋃ ran ((.) \circ F)$
56	54 55	syl	$⊢ φ \to ⋃_{x \in ℕ} ((.) \circ F) (x) = ⋃ ran ((.) \circ F)$
57		iunun	$⊢ ⋃_{x \in ℕ} (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\}) = ⋃_{x \in ℕ} \{(1^{st} \circ F) (x)\} \cup ⋃_{x \in ℕ} \{(2^{nd} \circ F) (x)\}$
58		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
59		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
60	58 59	ax-mp	$⊢ 1^{st} Fn V$
61		ssv	$⊢ \leq \cap ℝ^{2} \subseteq V$
62		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq V) \to F : ℕ ⟶ V$
63	1 61 62	sylancl	$⊢ φ \to F : ℕ ⟶ V$
64		fnfco	$⊢ (1^{st} Fn V \land F : ℕ ⟶ V) \to (1^{st} \circ F) Fn ℕ$
65	60 63 64	sylancr	$⊢ φ \to (1^{st} \circ F) Fn ℕ$
66		fnfun	$⊢ (1^{st} \circ F) Fn ℕ \to Fun (1^{st} \circ F)$
67	65 66	syl	$⊢ φ \to Fun (1^{st} \circ F)$
68		fndm	$⊢ (1^{st} \circ F) Fn ℕ \to dom (1^{st} \circ F) = ℕ$
69		eqimss2	$⊢ dom (1^{st} \circ F) = ℕ \to ℕ \subseteq dom (1^{st} \circ F)$
70	65 68 69	3syl	$⊢ φ \to ℕ \subseteq dom (1^{st} \circ F)$
71		dfimafn2	$⊢ (Fun (1^{st} \circ F) \land ℕ \subseteq dom (1^{st} \circ F)) \to (1^{st} \circ F) [ℕ] = ⋃_{x \in ℕ} \{(1^{st} \circ F) (x)\}$
72	67 70 71	syl2anc	$⊢ φ \to (1^{st} \circ F) [ℕ] = ⋃_{x \in ℕ} \{(1^{st} \circ F) (x)\}$
73		fnima	$⊢ (1^{st} \circ F) Fn ℕ \to (1^{st} \circ F) [ℕ] = ran (1^{st} \circ F)$
74	65 73	syl	$⊢ φ \to (1^{st} \circ F) [ℕ] = ran (1^{st} \circ F)$
75	72 74	eqtr3d	$⊢ φ \to ⋃_{x \in ℕ} \{(1^{st} \circ F) (x)\} = ran (1^{st} \circ F)$
76		rnco2	$⊢ ran (1^{st} \circ F) = 1^{st} [ran F]$
77	75 76	eqtrdi	$⊢ φ \to ⋃_{x \in ℕ} \{(1^{st} \circ F) (x)\} = 1^{st} [ran F]$
78		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
79		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
80	78 79	ax-mp	$⊢ 2^{nd} Fn V$
81		fnfco	$⊢ (2^{nd} Fn V \land F : ℕ ⟶ V) \to (2^{nd} \circ F) Fn ℕ$
82	80 63 81	sylancr	$⊢ φ \to (2^{nd} \circ F) Fn ℕ$
83		fnfun	$⊢ (2^{nd} \circ F) Fn ℕ \to Fun (2^{nd} \circ F)$
84	82 83	syl	$⊢ φ \to Fun (2^{nd} \circ F)$
85		fndm	$⊢ (2^{nd} \circ F) Fn ℕ \to dom (2^{nd} \circ F) = ℕ$
86		eqimss2	$⊢ dom (2^{nd} \circ F) = ℕ \to ℕ \subseteq dom (2^{nd} \circ F)$
87	82 85 86	3syl	$⊢ φ \to ℕ \subseteq dom (2^{nd} \circ F)$
88		dfimafn2	$⊢ (Fun (2^{nd} \circ F) \land ℕ \subseteq dom (2^{nd} \circ F)) \to (2^{nd} \circ F) [ℕ] = ⋃_{x \in ℕ} \{(2^{nd} \circ F) (x)\}$
89	84 87 88	syl2anc	$⊢ φ \to (2^{nd} \circ F) [ℕ] = ⋃_{x \in ℕ} \{(2^{nd} \circ F) (x)\}$
90		fnima	$⊢ (2^{nd} \circ F) Fn ℕ \to (2^{nd} \circ F) [ℕ] = ran (2^{nd} \circ F)$
91	82 90	syl	$⊢ φ \to (2^{nd} \circ F) [ℕ] = ran (2^{nd} \circ F)$
92	89 91	eqtr3d	$⊢ φ \to ⋃_{x \in ℕ} \{(2^{nd} \circ F) (x)\} = ran (2^{nd} \circ F)$
93		rnco2	$⊢ ran (2^{nd} \circ F) = 2^{nd} [ran F]$
94	92 93	eqtrdi	$⊢ φ \to ⋃_{x \in ℕ} \{(2^{nd} \circ F) (x)\} = 2^{nd} [ran F]$
95	77 94	uneq12d	$⊢ φ \to ⋃_{x \in ℕ} \{(1^{st} \circ F) (x)\} \cup ⋃_{x \in ℕ} \{(2^{nd} \circ F) (x)\} = 1^{st} [ran F] \cup 2^{nd} [ran F]$
96	57 95	eqtrid	$⊢ φ \to ⋃_{x \in ℕ} (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\}) = 1^{st} [ran F] \cup 2^{nd} [ran F]$
97	56 96	uneq12d	$⊢ φ \to ⋃_{x \in ℕ} ((.) \circ F) (x) \cup ⋃_{x \in ℕ} (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\}) = ⋃ ran ((.) \circ F) \cup (1^{st} [ran F] \cup 2^{nd} [ran F])$
98	49 97	eqtrid	$⊢ φ \to ⋃_{x \in ℕ} (((.) \circ F) (x) \cup (\{(1^{st} \circ F) (x)\} \cup \{(2^{nd} \circ F) (x)\})) = ⋃ ran ((.) \circ F) \cup (1^{st} [ran F] \cup 2^{nd} [ran F])$
99	36 48 98	3eqtr3d	$⊢ φ \to ⋃ ran ([.] \circ F) = ⋃ ran ((.) \circ F) \cup (1^{st} [ran F] \cup 2^{nd} [ran F])$
100	2 99	sseqtrrid	$⊢ φ \to ⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F)$
101		ovolficcss	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$
102	1 101	syl	$⊢ φ \to ⋃ ran ([.] \circ F) \subseteq ℝ$
103	102	ssdifssd	$⊢ φ \to ⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F) \subseteq ℝ$
104		omelon	$⊢ ω \in On$
105		nnenom	$⊢ ℕ \approx ω$
106	105	ensymi	$⊢ ω \approx ℕ$
107		isnumi	$⊢ (ω \in On \land ω \approx ℕ) \to ℕ \in dom card$
108	104 106 107	mp2an	$⊢ ℕ \in dom card$
109		fofun	$⊢ 1^{st} : V \underset{onto}{⟶} V \to Fun 1^{st}$
110	58 109	ax-mp	$⊢ Fun 1^{st}$
111		ssv	$⊢ ran F \subseteq V$
112		fof	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} : V ⟶ V$
113	58 112	ax-mp	$⊢ 1^{st} : V ⟶ V$
114	113	fdmi	$⊢ dom 1^{st} = V$
115	111 114	sseqtrri	$⊢ ran F \subseteq dom 1^{st}$
116		fores	$⊢ (Fun 1^{st} \land ran F \subseteq dom 1^{st}) \to ({1^{st} ↾}_{ran F}) : ran F \underset{onto}{⟶} 1^{st} [ran F]$
117	110 115 116	mp2an	$⊢ ({1^{st} ↾}_{ran F}) : ran F \underset{onto}{⟶} 1^{st} [ran F]$
118	1	ffnd	$⊢ φ \to F Fn ℕ$
119		dffn4	$⊢ F Fn ℕ \leftrightarrow F : ℕ \underset{onto}{⟶} ran F$
120	118 119	sylib	$⊢ φ \to F : ℕ \underset{onto}{⟶} ran F$
121		foco	$⊢ (({1^{st} ↾}_{ran F}) : ran F \underset{onto}{⟶} 1^{st} [ran F] \land F : ℕ \underset{onto}{⟶} ran F) \to (({1^{st} ↾}_{ran F}) \circ F) : ℕ \underset{onto}{⟶} 1^{st} [ran F]$
122	117 120 121	sylancr	$⊢ φ \to (({1^{st} ↾}_{ran F}) \circ F) : ℕ \underset{onto}{⟶} 1^{st} [ran F]$
123		fodomnum	$⊢ ℕ \in dom card \to ((({1^{st} ↾}_{ran F}) \circ F) : ℕ \underset{onto}{⟶} 1^{st} [ran F] \to 1^{st} [ran F] ≼ ℕ)$
124	108 122 123	mpsyl	$⊢ φ \to 1^{st} [ran F] ≼ ℕ$
125		domentr	$⊢ (1^{st} [ran F] ≼ ℕ \land ℕ \approx ω) \to 1^{st} [ran F] ≼ ω$
126	124 105 125	sylancl	$⊢ φ \to 1^{st} [ran F] ≼ ω$
127		fofun	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to Fun 2^{nd}$
128	78 127	ax-mp	$⊢ Fun 2^{nd}$
129		fof	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} : V ⟶ V$
130	78 129	ax-mp	$⊢ 2^{nd} : V ⟶ V$
131	130	fdmi	$⊢ dom 2^{nd} = V$
132	111 131	sseqtrri	$⊢ ran F \subseteq dom 2^{nd}$
133		fores	$⊢ (Fun 2^{nd} \land ran F \subseteq dom 2^{nd}) \to ({2^{nd} ↾}_{ran F}) : ran F \underset{onto}{⟶} 2^{nd} [ran F]$
134	128 132 133	mp2an	$⊢ ({2^{nd} ↾}_{ran F}) : ran F \underset{onto}{⟶} 2^{nd} [ran F]$
135		foco	$⊢ (({2^{nd} ↾}_{ran F}) : ran F \underset{onto}{⟶} 2^{nd} [ran F] \land F : ℕ \underset{onto}{⟶} ran F) \to (({2^{nd} ↾}_{ran F}) \circ F) : ℕ \underset{onto}{⟶} 2^{nd} [ran F]$
136	134 120 135	sylancr	$⊢ φ \to (({2^{nd} ↾}_{ran F}) \circ F) : ℕ \underset{onto}{⟶} 2^{nd} [ran F]$
137		fodomnum	$⊢ ℕ \in dom card \to ((({2^{nd} ↾}_{ran F}) \circ F) : ℕ \underset{onto}{⟶} 2^{nd} [ran F] \to 2^{nd} [ran F] ≼ ℕ)$
138	108 136 137	mpsyl	$⊢ φ \to 2^{nd} [ran F] ≼ ℕ$
139		domentr	$⊢ (2^{nd} [ran F] ≼ ℕ \land ℕ \approx ω) \to 2^{nd} [ran F] ≼ ω$
140	138 105 139	sylancl	$⊢ φ \to 2^{nd} [ran F] ≼ ω$
141		unctb	$⊢ (1^{st} [ran F] ≼ ω \land 2^{nd} [ran F] ≼ ω) \to (1^{st} [ran F] \cup 2^{nd} [ran F]) ≼ ω$
142	126 140 141	syl2anc	$⊢ φ \to (1^{st} [ran F] \cup 2^{nd} [ran F]) ≼ ω$
143		ctex	$⊢ (1^{st} [ran F] \cup 2^{nd} [ran F]) ≼ ω \to 1^{st} [ran F] \cup 2^{nd} [ran F] \in V$
144	142 143	syl	$⊢ φ \to 1^{st} [ran F] \cup 2^{nd} [ran F] \in V$
145		ssid	$⊢ ⋃ ran ([.] \circ F) \subseteq ⋃ ran ([.] \circ F)$
146	145 99	sseqtrid	$⊢ φ \to ⋃ ran ([.] \circ F) \subseteq ⋃ ran ((.) \circ F) \cup (1^{st} [ran F] \cup 2^{nd} [ran F])$
147		ssundif	$⊢ ⋃ ran ([.] \circ F) \subseteq ⋃ ran ((.) \circ F) \cup (1^{st} [ran F] \cup 2^{nd} [ran F]) \leftrightarrow ⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F) \subseteq 1^{st} [ran F] \cup 2^{nd} [ran F]$
148	146 147	sylib	$⊢ φ \to ⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F) \subseteq 1^{st} [ran F] \cup 2^{nd} [ran F]$
149		ssdomg	$⊢ 1^{st} [ran F] \cup 2^{nd} [ran F] \in V \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F) \subseteq 1^{st} [ran F] \cup 2^{nd} [ran F] \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ (1^{st} [ran F] \cup 2^{nd} [ran F]))$
150	144 148 149	sylc	$⊢ φ \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ (1^{st} [ran F] \cup 2^{nd} [ran F])$
151		domtr	$⊢ ((⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ (1^{st} [ran F] \cup 2^{nd} [ran F]) \land (1^{st} [ran F] \cup 2^{nd} [ran F]) ≼ ω) \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ ω$
152	150 142 151	syl2anc	$⊢ φ \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ ω$
153		domentr	$⊢ ((⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ ω \land ω \approx ℕ) \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ ℕ$
154	152 106 153	sylancl	$⊢ φ \to (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ ℕ$
155		ovolctb2	$⊢ (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F) \subseteq ℝ \land (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) ≼ ℕ) \to {vol}^{*} (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) = 0$
156	103 154 155	syl2anc	$⊢ φ \to {vol}^{*} (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) = 0$
157	100 156	jca	$⊢ φ \to (⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F) \land {vol}^{*} (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) = 0)$

Metamath Proof Explorer

Theorem uniiccdif

Proof