Theorem vitalilem5 25780

Description: Lemma for vitali 25781. (Contributed by Mario Carneiro, 16-Jun-2014.)

Hypotheses

Ref	Expression
vitali.1	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
vitali.2	⊢ 𝑆 = ((0[,]1) / ∼ )
vitali.3	⊢ (𝜑 → 𝐹 Fn 𝑆)
vitali.4	⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
vitali.5	⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
vitali.6	⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
vitali.7	⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))

Assertion

Ref	Expression
vitalilem5	⊢ ¬ 𝜑

Distinct variable groups:   𝑛,𝑠,𝑥,𝑦,𝑧,𝐺   𝜑,𝑛,𝑥,𝑧   𝑧,𝑆   𝑥,𝑇   𝑛,𝐹,𝑠,𝑥,𝑦,𝑧   ∼ ,𝑛,𝑠,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑦, 𝑠)   𝑆(𝑥, 𝑦, 𝑛, 𝑠)   𝑇(𝑦, 𝑧, 𝑛, 𝑠)

Proof of Theorem vitalilem5

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0lt1 11740	. . . 4 ⊢ 0 < 1
2		0re 11214	. . . . . 6 ⊢ 0 ∈ ℝ
3		1re 11212	. . . . . 6 ⊢ 1 ∈ ℝ
4		0le1 11741	. . . . . 6 ⊢ 0 ≤ 1
5		ovolicc 25691	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) → (vol*‘(0[,]1)) = (1 − 0))
6	2, 3, 4, 5	mp3an 1490	. . . . 5 ⊢ (vol*‘(0[,]1)) = (1 − 0)
7		1m0e1 12364	. . . . 5 ⊢ (1 − 0) = 1
8	6, 7	eqtri 2786	. . . 4 ⊢ (vol*‘(0[,]1)) = 1
9	1, 8	breqtrri 5138	. . 3 ⊢ 0 < (vol*‘(0[,]1))
10	8, 3	eqeltri 2859	. . . 4 ⊢ (vol*‘(0[,]1)) ∈ ℝ
11	2, 10	ltnlei 11335	. . 3 ⊢ (0 < (vol*‘(0[,]1)) ↔ ¬ (vol*‘(0[,]1)) ≤ 0)
12	9, 11	mpbi 233	. 2 ⊢ ¬ (vol*‘(0[,]1)) ≤ 0
13		vitali.1	. . . . . 6 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
14		vitali.2	. . . . . 6 ⊢ 𝑆 = ((0[,]1) / ∼ )
15		vitali.3	. . . . . 6 ⊢ (𝜑 → 𝐹 Fn 𝑆)
16		vitali.4	. . . . . 6 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
17		vitali.5	. . . . . 6 ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
18		vitali.6	. . . . . 6 ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
19		vitali.7	. . . . . 6 ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
20	13, 14, 15, 16, 17, 18, 19	vitalilem2 25777	. . . . 5 ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)))
21	20	simp2d 1161	. . . 4 ⊢ (𝜑 → (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚))
22	13	vitalilem1 25776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∼ Er (0[,]1)
23		erdm 8701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ∼ Er (0[,]1) → dom ∼ = (0[,]1))
24	22, 23	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom ∼ = (0[,]1)
25		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆)
26	25, 14	eleqtrdi 2873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((0[,]1) / ∼ ))
27		elqsn0 8778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((dom ∼ = (0[,]1) ∧ 𝑧 ∈ ((0[,]1) / ∼ )) → 𝑧 ≠ ∅)
28	24, 26, 27	sylancr 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ≠ ∅)
29	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∼ Er (0[,]1))
30	29	qsss 8769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((0[,]1) / ∼ ) ⊆ 𝒫 (0[,]1))
31	14, 30	eqsstrid 3975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑆 ⊆ 𝒫 (0[,]1))
32	31	sselda 3937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝒫 (0[,]1))
33	32	elpwid 4571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ⊆ (0[,]1))
34	33	sseld 3936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) ∈ 𝑧 → (𝐹‘𝑧) ∈ (0[,]1)))
35	28, 34	embantd 60	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → (𝐹‘𝑧) ∈ (0[,]1)))
36	35	ralimdva 3177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1)))
37	16, 36	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))
38		ffnfv 7114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1)))
39	15, 37, 38	sylanbrc 594	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝑆⟶(0[,]1))
40	39	frnd 6714	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1))
41		unitssre 13530	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
42	40, 41	sstrdi 3949	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
43		reex 11195	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
44	43	elpw2 5305	. . . . . . . . . . . . . . 15 ⊢ (ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
45	42, 44	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 ∈ 𝒫 ℝ)
46	45	anim1i 626	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol))
47		eldif 3915	. . . . . . . . . . . . 13 ⊢ (ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol) ↔ (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol))
48	46, 47	sylibr 237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
49	48	ex 417	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol)))
50	19, 49	mt3d 149	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 ∈ dom vol)
51		f1of 6820	. . . . . . . . . . . . 13 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
52	17, 51	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
53		inss1 4189	. . . . . . . . . . . . 13 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℚ
54		qssre 12987	. . . . . . . . . . . . 13 ⊢ ℚ ⊆ ℝ
55	53, 54	sstri 3946	. . . . . . . . . . . 12 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℝ
56		fss 6722	. . . . . . . . . . . 12 ⊢ ((𝐺:ℕ⟶(ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℝ) → 𝐺:ℕ⟶ℝ)
57	52, 55, 56	sylancl 597	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:ℕ⟶ℝ)
58	57	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ)
59		shftmbl 25706	. . . . . . . . . 10 ⊢ ((ran 𝐹 ∈ dom vol ∧ (𝐺‘𝑛) ∈ ℝ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol)
60	50, 58, 59	syl2an2r 697	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol)
61	60, 18	fmptd 7109	. . . . . . . 8 ⊢ (𝜑 → 𝑇:ℕ⟶dom vol)
62	61	ffvelcdmda 7079	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ∈ dom vol)
63	62	ralrimiva 3157	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
64		iunmbl 25721	. . . . . 6 ⊢ (∀𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
65	63, 64	syl 18	. . . . 5 ⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
66		mblss 25699	. . . . 5 ⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ)
67	65, 66	syl 18	. . . 4 ⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ)
68		ovolss 25653	. . . 4 ⊢ (((0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ) → (vol*‘(0[,]1)) ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
69	21, 67, 68	syl2anc 595	. . 3 ⊢ (𝜑 → (vol*‘(0[,]1)) ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
70		eqid 2763	. . . . . 6 ⊢ seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))))
71		eqid 2763	. . . . . 6 ⊢ (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))
72		mblss 25699	. . . . . . 7 ⊢ ((𝑇‘𝑚) ∈ dom vol → (𝑇‘𝑚) ⊆ ℝ)
73	62, 72	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ⊆ ℝ)
74	13, 14, 15, 16, 17, 18, 19	vitalilem4 25779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0)
75	74, 2	eqeltrdi 2871	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) ∈ ℝ)
76	74	mpteq2dva 5204	. . . . . . . . . 10 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ 0))
77		fconstmpt 5723	. . . . . . . . . . 11 ⊢ (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
78		nnuz 12905	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
79	78	xpeq1i 5687	. . . . . . . . . . 11 ⊢ (ℕ × {0}) = ((ℤ≥‘1) × {0})
80	77, 79	eqtr3i 2788	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ ↦ 0) = ((ℤ≥‘1) × {0})
81	76, 80	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚))) = ((ℤ≥‘1) × {0}))
82	81	seqeq3d 14050	. . . . . . . 8 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) = seq1( + , ((ℤ≥‘1) × {0})))
83		1z 12628	. . . . . . . . 9 ⊢ 1 ∈ ℤ
84		serclim0 15633	. . . . . . . . 9 ⊢ (1 ∈ ℤ → seq1( + , ((ℤ≥‘1) × {0})) ⇝ 0)
85	83, 84	ax-mp 5	. . . . . . . 8 ⊢ seq1( + , ((ℤ≥‘1) × {0})) ⇝ 0
86	82, 85	eqbrtrdi 5150	. . . . . . 7 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) ⇝ 0)
87		seqex 14044	. . . . . . . 8 ⊢ seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) ∈ V
88		c0ex 11204	. . . . . . . 8 ⊢ 0 ∈ V
89	87, 88	breldm 5898	. . . . . . 7 ⊢ (seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) ⇝ 0 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) ∈ dom ⇝ )
90	86, 89	syl 18	. . . . . 6 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇‘𝑚)))) ∈ dom ⇝ )
91	70, 71, 73, 75, 90	ovoliun2 25674	. . . . 5 ⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)))
92	74	sumeq2dv 15758	. . . . . 6 ⊢ (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)) = Σ𝑚 ∈ ℕ 0)
93	78	eqimssi 3997	. . . . . . . 8 ⊢ ℕ ⊆ (ℤ≥‘1)
94	93	orci 878	. . . . . . 7 ⊢ (ℕ ⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin)
95		sumz 15778	. . . . . . 7 ⊢ ((ℕ ⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin) → Σ𝑚 ∈ ℕ 0 = 0)
96	94, 95	ax-mp 5	. . . . . 6 ⊢ Σ𝑚 ∈ ℕ 0 = 0
97	92, 96	eqtrdi 2814	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇‘𝑚)) = 0)
98	91, 97	breqtrd 5137	. . . 4 ⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0)
99		ovolge0 25649	. . . . 5 ⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
100	67, 99	syl 18	. . . 4 ⊢ (𝜑 → 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
101		ovolcl 25646	. . . . . 6 ⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ*)
102	67, 101	syl 18	. . . . 5 ⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ*)
103		0xr 11260	. . . . 5 ⊢ 0 ∈ ℝ*
104		xrletri3 13183	. . . . 5 ⊢ (((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0 ↔ ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))))
105	102, 103, 104	sylancl 597	. . . 4 ⊢ (𝜑 → ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0 ↔ ((vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))))
106	98, 100, 105	mpbir2and 725	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = 0)
107	69, 106	breqtrd 5137	. 2 ⊢ (𝜑 → (vol*‘(0[,]1)) ≤ 0)
108	12, 107	mto 200	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  {crab 3416   ∖ cdif 3902   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4562  {csn 4589  ∪ ciun 4956   class class class wbr 5109  {copab 5173   ↦ cmpt 5192   × cxp 5659  dom cdm 5661  ran crn 5662   Fn wfn 6531  ⟶wf 6532  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410   Er wer 8687   / cqs 8689  Fincfn 8939  ℝcr 11103  0cc0 11104  1c1 11105   + caddc 11107  ℝ^*cxr 11246   < clt 11247   ≤ cle 11248   − cmin 11445  -cneg 11446  ℕcn 12237  2c2 12299  ℤcz 12595  ℤ_≥cuz 12866  ℚcq 12976  [,]cicc 13379  seqcseq 14042   ⇝ cli 15540  Σcsu 15742  vol*covol 25630  volcvol 25631

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cc 10423  ax-cnex 11160  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181  ax-pre-sup 11182

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-disj 5077  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-ec 8692  df-qs 8696  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-dju 9892  df-card 9930  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-div 11876  df-nn 12238  df-2 12307  df-3 12308  df-n0 12509  df-z 12596  df-uz 12867  df-q 12977  df-rp 13021  df-xneg 13141  df-xadd 13142  df-xmul 13143  df-ioo 13380  df-ico 13382  df-icc 13383  df-fz 13540  df-fzo 13688  df-fl 13830  df-seq 14043  df-exp 14103  df-hash 14372  df-cj 15155  df-re 15156  df-im 15157  df-sqrt 15291  df-abs 15292  df-clim 15544  df-rlim 15545  df-sum 15743  df-rest 17479  df-topgen 17500  df-psmet 21523  df-xmet 21524  df-met 21525  df-bl 21526  df-mopn 21527  df-top 23060  df-topon 23077  df-bases 23112  df-cmp 23553  df-ovol 25632  df-vol 25633

This theorem is used by:  vitali  25781