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	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	Assertion	uniiccdif	⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = 0 ) )

Proof

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

Metamath Proof Explorer

Theorem uniiccdif

Proof