ovoliunnfl

Description: ovoliun is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017)

		Ref	Expression
	Hypothesis	ovoliunnfl.0	$⊢ (f Fn ℕ \land \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)) \to {vol}^{} (⋃_{m \in ℕ} f (m)) \leq sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{} <)$
	Assertion	ovoliunnfl	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Proof

Step	Hyp	Ref	Expression
1		ovoliunnfl.0	$⊢ (f Fn ℕ \land \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)) \to {vol}^{} (⋃_{m \in ℕ} f (m)) \leq sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{} <)$
2		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
3		uni0	$⊢ ⋃ \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ A = \emptyset \to ⋃ A = \emptyset$
5	4	fveq2d	$⊢ A = \emptyset \to {vol}^{} (⋃ A) = {vol}^{} (\emptyset)$
6		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
7	5 6	eqtr2di	$⊢ A = \emptyset \to 0 = {vol}^{*} (⋃ A)$
8	7	a1d	$⊢ A = \emptyset \to ((A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = {vol}^{*} (⋃ A))$
9		ovolge0	$⊢ ⋃ A \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ A)$
10	9	ad2antll	$⊢ ((A \neq \emptyset \land A ≼ ℕ) \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 \leq {vol}^{*} (⋃ A)$
11		reldom	$⊢ Rel ≼$
12	11	brrelex1i	$⊢ A ≼ ℕ \to A \in V$
13		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
14	12 13	syl	$⊢ A ≼ ℕ \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
15	14	biimparc	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to \emptyset ≺ A$
16		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} A$
17	15 16	sylancom	$⊢ (A \neq \emptyset \land A ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} A$
18		unissb	$⊢ ⋃ A \subseteq ℝ \leftrightarrow \forall x \in A x \subseteq ℝ$
19	18	anbi1i	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \leftrightarrow (\forall x \in A x \subseteq ℝ \land \forall x \in A x ≼ ℕ)$
20		r19.26	$⊢ \forall x \in A (x \subseteq ℝ \land x ≼ ℕ) \leftrightarrow (\forall x \in A x \subseteq ℝ \land \forall x \in A x ≼ ℕ)$
21	19 20	bitr4i	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \leftrightarrow \forall x \in A (x \subseteq ℝ \land x ≼ ℕ)$
22		brdom2	$⊢ x ≼ ℕ \leftrightarrow (x ≺ ℕ \lor x \approx ℕ)$
23		nnenom	$⊢ ℕ \approx ω$
24		sdomen2	$⊢ ℕ \approx ω \to (x ≺ ℕ \leftrightarrow x ≺ ω)$
25	23 24	ax-mp	$⊢ x ≺ ℕ \leftrightarrow x ≺ ω$
26		isfinite	$⊢ x \in Fin \leftrightarrow x ≺ ω$
27	25 26	bitr4i	$⊢ x ≺ ℕ \leftrightarrow x \in Fin$
28	27	orbi1i	$⊢ (x ≺ ℕ \lor x \approx ℕ) \leftrightarrow (x \in Fin \lor x \approx ℕ)$
29	22 28	bitri	$⊢ x ≼ ℕ \leftrightarrow (x \in Fin \lor x \approx ℕ)$
30		ovolfi	$⊢ (x \in Fin \land x \subseteq ℝ) \to {vol}^{*} (x) = 0$
31	30	expcom	$⊢ x \subseteq ℝ \to (x \in Fin \to {vol}^{*} (x) = 0)$
32		ovolctb	$⊢ (x \subseteq ℝ \land x \approx ℕ) \to {vol}^{*} (x) = 0$
33	32	ex	$⊢ x \subseteq ℝ \to (x \approx ℕ \to {vol}^{*} (x) = 0)$
34	31 33	jaod	$⊢ x \subseteq ℝ \to ((x \in Fin \lor x \approx ℕ) \to {vol}^{*} (x) = 0)$
35	29 34	syl5bi	$⊢ x \subseteq ℝ \to (x ≼ ℕ \to {vol}^{*} (x) = 0)$
36	35	imdistani	$⊢ (x \subseteq ℝ \land x ≼ ℕ) \to (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
37	36	ralimi	$⊢ \forall x \in A (x \subseteq ℝ \land x ≼ ℕ) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
38	21 37	sylbi	$⊢ (⋃ A \subseteq ℝ \land \forall x \in A x ≼ ℕ) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
39	38	ancoms	$⊢ (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ) \to \forall x \in A (x \subseteq ℝ \land {vol}^{*} (x) = 0)$
40		foima	$⊢ f : ℕ \underset{onto}{⟶} A \to f [ℕ] = A$
41	40	raleqdv	$⊢ f : ℕ \underset{onto}{⟶} A \to (\forall x \in f [ℕ] (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0))$
42		fofn	$⊢ f : ℕ \underset{onto}{⟶} A \to f Fn ℕ$
43		ssid	$⊢ ℕ \subseteq ℕ$
44		sseq1	$⊢ x = f (l) \to (x \subseteq ℝ \leftrightarrow f (l) \subseteq ℝ)$
45		fveqeq2	$⊢ x = f (l) \to ({vol}^{} (x) = 0 \leftrightarrow {vol}^{} (f (l)) = 0)$
46	44 45	anbi12d	$⊢ x = f (l) \to ((x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0))$
47	46	ralima	$⊢ (f Fn ℕ \land ℕ \subseteq ℕ) \to (\forall x \in f [ℕ] (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0))$
48	42 43 47	sylancl	$⊢ f : ℕ \underset{onto}{⟶} A \to (\forall x \in f [ℕ] (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0))$
49	41 48	bitr3d	$⊢ f : ℕ \underset{onto}{⟶} A \to (\forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0) \leftrightarrow \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0))$
50		fveq2	$⊢ l = n \to f (l) = f (n)$
51	50	sseq1d	$⊢ l = n \to (f (l) \subseteq ℝ \leftrightarrow f (n) \subseteq ℝ)$
52		2fveq3	$⊢ l = n \to {vol}^{} (f (l)) = {vol}^{} (f (n))$
53	52	eqeq1d	$⊢ l = n \to ({vol}^{} (f (l)) = 0 \leftrightarrow {vol}^{} (f (n)) = 0)$
54	51 53	anbi12d	$⊢ l = n \to ((f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \leftrightarrow (f (n) \subseteq ℝ \land {vol}^{} (f (n)) = 0))$
55	54	cbvralvw	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \leftrightarrow \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) = 0)$
56		0re	$⊢ 0 \in ℝ$
57		eleq1a	$⊢ 0 \in ℝ \to ({vol}^{} (f (n)) = 0 \to {vol}^{} (f (n)) \in ℝ)$
58	56 57	ax-mp	$⊢ {vol}^{} (f (n)) = 0 \to {vol}^{} (f (n)) \in ℝ$
59	58	anim2i	$⊢ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) = 0) \to (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)$
60	59	ralimi	$⊢ \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) = 0) \to \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)$
61	55 60	sylbi	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)$
62	42 61 1	syl2an	$⊢ (f : ℕ \underset{onto}{⟶} A \land \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0)) \to {vol}^{} (⋃_{m \in ℕ} f (m)) \leq sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{} <)$
63		fofun	$⊢ f : ℕ \underset{onto}{⟶} A \to Fun f$
64		funiunfv	$⊢ Fun f \to ⋃_{m \in ℕ} f (m) = ⋃ f [ℕ]$
65	63 64	syl	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃_{m \in ℕ} f (m) = ⋃ f [ℕ]$
66	40	unieqd	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃ f [ℕ] = ⋃ A$
67	65 66	eqtrd	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃_{m \in ℕ} f (m) = ⋃ A$
68	67	fveq2d	$⊢ f : ℕ \underset{onto}{⟶} A \to {vol}^{} (⋃_{m \in ℕ} f (m)) = {vol}^{} (⋃ A)$
69	68	adantr	$⊢ (f : ℕ \underset{onto}{⟶} A \land \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0)) \to {vol}^{} (⋃_{m \in ℕ} f (m)) = {vol}^{*} (⋃ A)$
70		fveq2	$⊢ l = m \to f (l) = f (m)$
71	70	sseq1d	$⊢ l = m \to (f (l) \subseteq ℝ \leftrightarrow f (m) \subseteq ℝ)$
72		2fveq3	$⊢ l = m \to {vol}^{} (f (l)) = {vol}^{} (f (m))$
73	72	eqeq1d	$⊢ l = m \to ({vol}^{} (f (l)) = 0 \leftrightarrow {vol}^{} (f (m)) = 0)$
74	71 73	anbi12d	$⊢ l = m \to ((f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \leftrightarrow (f (m) \subseteq ℝ \land {vol}^{} (f (m)) = 0))$
75	74	rspccva	$⊢ (\forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \land m \in ℕ) \to (f (m) \subseteq ℝ \land {vol}^{} (f (m)) = 0)$
76	75	simprd	$⊢ (\forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \land m \in ℕ) \to {vol}^{} (f (m)) = 0$
77	76	mpteq2dva	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to (m \in ℕ ⟼ {vol}^{} (f (m))) = (m \in ℕ ⟼ 0)$
78	77	seqeq3d	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) = seq 1 (+ (m \in ℕ ⟼ 0))$
79	78	rneqd	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) = ran seq 1 (+ (m \in ℕ ⟼ 0))$
80	79	supeq1d	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{} <) = sup (ran seq 1 (+ (m \in ℕ ⟼ 0)) ℝ^{} <)$
81		0cn	$⊢ 0 \in ℂ$
82		ser1const	$⊢ (0 \in ℂ \land l \in ℕ) \to seq 1 (+ (ℕ \times \{0\})) (l) = l \cdot 0$
83	81 82	mpan	$⊢ l \in ℕ \to seq 1 (+ (ℕ \times \{0\})) (l) = l \cdot 0$
84		nncn	$⊢ l \in ℕ \to l \in ℂ$
85	84	mul01d	$⊢ l \in ℕ \to l \cdot 0 = 0$
86	83 85	eqtrd	$⊢ l \in ℕ \to seq 1 (+ (ℕ \times \{0\})) (l) = 0$
87	86	mpteq2ia	$⊢ (l \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (l)) = (l \in ℕ ⟼ 0)$
88		fconstmpt	$⊢ ℕ \times \{0\} = (m \in ℕ ⟼ 0)$
89		seqeq3	$⊢ ℕ \times \{0\} = (m \in ℕ ⟼ 0) \to seq 1 (+ (ℕ \times \{0\})) = seq 1 (+ (m \in ℕ ⟼ 0))$
90	88 89	ax-mp	$⊢ seq 1 (+ (ℕ \times \{0\})) = seq 1 (+ (m \in ℕ ⟼ 0))$
91		1z	$⊢ 1 \in ℤ$
92		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1}$
93	91 92	ax-mp	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1}$
94		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
95	94	fneq2i	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℕ \leftrightarrow seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1}$
96		dffn5	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℕ \leftrightarrow seq 1 (+ (ℕ \times \{0\})) = (l \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (l))$
97	95 96	bitr3i	$⊢ seq 1 (+ (ℕ \times \{0\})) Fn ℤ_{\geq 1} \leftrightarrow seq 1 (+ (ℕ \times \{0\})) = (l \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (l))$
98	93 97	mpbi	$⊢ seq 1 (+ (ℕ \times \{0\})) = (l \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (l))$
99	90 98	eqtr3i	$⊢ seq 1 (+ (m \in ℕ ⟼ 0)) = (l \in ℕ ⟼ seq 1 (+ (ℕ \times \{0\})) (l))$
100		fconstmpt	$⊢ ℕ \times \{0\} = (l \in ℕ ⟼ 0)$
101	87 99 100	3eqtr4i	$⊢ seq 1 (+ (m \in ℕ ⟼ 0)) = ℕ \times \{0\}$
102	101	rneqi	$⊢ ran seq 1 (+ (m \in ℕ ⟼ 0)) = ran (ℕ \times \{0\})$
103		1nn	$⊢ 1 \in ℕ$
104		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
105		rnxp	$⊢ ℕ \neq \emptyset \to ran (ℕ \times \{0\}) = \{0\}$
106	103 104 105	mp2b	$⊢ ran (ℕ \times \{0\}) = \{0\}$
107	102 106	eqtri	$⊢ ran seq 1 (+ (m \in ℕ ⟼ 0)) = \{0\}$
108	107	supeq1i	$⊢ sup (ran seq 1 (+ (m \in ℕ ⟼ 0)) ℝ^{} <) = sup (\{0\} ℝ^{} <)$
109		xrltso	$⊢ < Or ℝ^{*}$
110		0xr	$⊢ 0 \in ℝ^{*}$
111		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
112	109 110 111	mp2an	$⊢ sup (\{0\} ℝ^{*} <) = 0$
113	108 112	eqtri	$⊢ sup (ran seq 1 (+ (m \in ℕ ⟼ 0)) ℝ^{*} <) = 0$
114	80 113	eqtrdi	$⊢ \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{*} <) = 0$
115	114	adantl	$⊢ (f : ℕ \underset{onto}{⟶} A \land \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0)) \to sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{*} <) = 0$
116	62 69 115	3brtr3d	$⊢ (f : ℕ \underset{onto}{⟶} A \land \forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0)) \to {vol}^{} (⋃ A) \leq 0$
117	116	ex	$⊢ f : ℕ \underset{onto}{⟶} A \to (\forall l \in ℕ (f (l) \subseteq ℝ \land {vol}^{} (f (l)) = 0) \to {vol}^{} (⋃ A) \leq 0)$
118	49 117	sylbid	$⊢ f : ℕ \underset{onto}{⟶} A \to (\forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0) \to {vol}^{} (⋃ A) \leq 0)$
119	118	exlimiv	$⊢ \exists f f : ℕ \underset{onto}{⟶} A \to (\forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0) \to {vol}^{} (⋃ A) \leq 0)$
120	119	imp	$⊢ (\exists f f : ℕ \underset{onto}{⟶} A \land \forall x \in A (x \subseteq ℝ \land {vol}^{} (x) = 0)) \to {vol}^{} (⋃ A) \leq 0$
121	17 39 120	syl2an	$⊢ ((A \neq \emptyset \land A ≼ ℕ) \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to {vol}^{*} (⋃ A) \leq 0$
122		ovolcl	$⊢ ⋃ A \subseteq ℝ \to {vol}^{} (⋃ A) \in ℝ^{}$
123		xrletri3	$⊢ (0 \in ℝ^{} \land {vol}^{} (⋃ A) \in ℝ^{}) \to (0 = {vol}^{} (⋃ A) \leftrightarrow (0 \leq {vol}^{} (⋃ A) \land {vol}^{} (⋃ A) \leq 0))$
124	110 122 123	sylancr	$⊢ ⋃ A \subseteq ℝ \to (0 = {vol}^{} (⋃ A) \leftrightarrow (0 \leq {vol}^{} (⋃ A) \land {vol}^{*} (⋃ A) \leq 0))$
125	124	ad2antll	$⊢ ((A \neq \emptyset \land A ≼ ℕ) \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to (0 = {vol}^{} (⋃ A) \leftrightarrow (0 \leq {vol}^{} (⋃ A) \land {vol}^{*} (⋃ A) \leq 0))$
126	10 121 125	mpbir2and	$⊢ ((A \neq \emptyset \land A ≼ ℕ) \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = {vol}^{*} (⋃ A)$
127	126	expl	$⊢ A \neq \emptyset \to ((A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = {vol}^{*} (⋃ A))$
128	8 127	pm2.61ine	$⊢ (A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to 0 = {vol}^{*} (⋃ A)$
129		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
130	56 129	mp1i	$⊢ ⋃ A = ℝ \to 0 \neq +∞$
131		fveq2	$⊢ ⋃ A = ℝ \to {vol}^{} (⋃ A) = {vol}^{} (ℝ)$
132		ovolre	$⊢ {vol}^{*} (ℝ) = +∞$
133	131 132	eqtrdi	$⊢ ⋃ A = ℝ \to {vol}^{*} (⋃ A) = +∞$
134	130 133	neeqtrrd	$⊢ ⋃ A = ℝ \to 0 \neq {vol}^{*} (⋃ A)$
135	134	necon2i	$⊢ 0 = {vol}^{*} (⋃ A) \to ⋃ A \neq ℝ$
136	128 135	syl	$⊢ (A ≼ ℕ \land (\forall x \in A x ≼ ℕ \land ⋃ A \subseteq ℝ)) \to ⋃ A \neq ℝ$
137	136	expr	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to (⋃ A \subseteq ℝ \to ⋃ A \neq ℝ)$
138		eqimss	$⊢ ⋃ A = ℝ \to ⋃ A \subseteq ℝ$
139	138	necon3bi	$⊢ \neg ⋃ A \subseteq ℝ \to ⋃ A \neq ℝ$
140	137 139	pm2.61d1	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Metamath Proof Explorer

Theorem ovoliunnfl

Proof