0ome - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 0ome		Structured version Visualization version GIF version

Theorem 0ome 47633

Description: The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypotheses**
Ref	Expression
0ome.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)
0ome.2	⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0)

**Assertion**
Ref	Expression
0ome	⊢ (𝜑 → 𝑂 ∈ OutMeas)

Distinct variable group: 𝑥,𝑋 Allowed substitution hints: 𝜑(𝑥) 𝑂(𝑥) 𝑉(𝑥)

Proof of Theorem 0ome Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2760	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝑋 ↦ 0) = (𝑦 ∈ 𝒫 𝑋 ↦ 0)
2		0e0iccpnf 13594	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝑋 → 0 ∈ (0[,]+∞))
4	1, 3	fmpti 7113	. . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 𝑋 ↦ 0):𝒫 𝑋⟶(0[,]+∞)
5		0ome.2	. . . . . . . . . . 11 ⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0)
6		eqidd 2761	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → 0 = 0)
7	6	cbvmptv 5208	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑋 ↦ 0) = (𝑦 ∈ 𝒫 𝑋 ↦ 0)
8	5, 7	eqtri 2783	. . . . . . . . . 10 ⊢ 𝑂 = (𝑦 ∈ 𝒫 𝑋 ↦ 0)
9	8	feq1i 6701	. . . . . . . . 9 ⊢ (𝑂:dom 𝑂⟶(0[,]+∞) ↔ (𝑦 ∈ 𝒫 𝑋 ↦ 0):dom 𝑂⟶(0[,]+∞))
10	8	dmeqi 5885	. . . . . . . . . . 11 ⊢ dom 𝑂 = dom (𝑦 ∈ 𝒫 𝑋 ↦ 0)
11		0re 11314	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
12	11	rgenw 3080	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ 𝒫 𝑋0 ∈ ℝ
13		dmmptg 6243	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝒫 𝑋0 ∈ ℝ → dom (𝑦 ∈ 𝒫 𝑋 ↦ 0) = 𝒫 𝑋)
14	12, 13	ax-mp 5	. . . . . . . . . . 11 ⊢ dom (𝑦 ∈ 𝒫 𝑋 ↦ 0) = 𝒫 𝑋
15	10, 14	eqtri 2783	. . . . . . . . . 10 ⊢ dom 𝑂 = 𝒫 𝑋
16	15	feq2i 6702	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝒫 𝑋 ↦ 0):dom 𝑂⟶(0[,]+∞) ↔ (𝑦 ∈ 𝒫 𝑋 ↦ 0):𝒫 𝑋⟶(0[,]+∞))
17	9, 16	bitri 278	. . . . . . . 8 ⊢ (𝑂:dom 𝑂⟶(0[,]+∞) ↔ (𝑦 ∈ 𝒫 𝑋 ↦ 0):𝒫 𝑋⟶(0[,]+∞))
18	4, 17	mpbir 234	. . . . . . 7 ⊢ 𝑂:dom 𝑂⟶(0[,]+∞)
19		unipw 5417	. . . . . . . . . 10 ⊢ ∪ 𝒫 𝑋 = 𝑋
20	19	pweqi 4572	. . . . . . . . 9 ⊢ 𝒫 ∪ 𝒫 𝑋 = 𝒫 𝑋
21	20	eqcomi 2769	. . . . . . . 8 ⊢ 𝒫 𝑋 = 𝒫 ∪ 𝒫 𝑋
22	15	eqcomi 2769	. . . . . . . . . 10 ⊢ 𝒫 𝑋 = dom 𝑂
23	22	unieqi 4878	. . . . . . . . 9 ⊢ ∪ 𝒫 𝑋 = ∪ dom 𝑂
24	23	pweqi 4572	. . . . . . . 8 ⊢ 𝒫 ∪ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
25	15, 21, 24	3eqtri 2787	. . . . . . 7 ⊢ dom 𝑂 = 𝒫 ∪ dom 𝑂
26	18, 25	pm3.2i 476	. . . . . 6 ⊢ (𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂)
27		0elpw 5316	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑋
28		eqidd 2761	. . . . . . . 8 ⊢ (𝑦 = ∅ → 0 = 0)
29	11	elexi 3472	. . . . . . . 8 ⊢ 0 ∈ V
30	28, 8, 29	fvmpt 6994	. . . . . . 7 ⊢ (∅ ∈ 𝒫 𝑋 → (𝑂‘∅) = 0)
31	27, 30	ax-mp 5	. . . . . 6 ⊢ (𝑂‘∅) = 0
32	26, 31	pm3.2i 476	. . . . 5 ⊢ ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0)
33	11	leidi 11854	. . . . . . . . 9 ⊢ 0 ≤ 0
34	33	a1i 11	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 0 ≤ 0)
35		eqidd 2761	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → 0 = 0)
36		elpwi 4563	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝒫 𝑦 → 𝑧 ⊆ 𝑦)
37	36	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ⊆ 𝑦)
38		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ∈ 𝒫 ∪ dom 𝑂)
39	21, 24	eqtr2i 2784	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 ∪ dom 𝑂 = 𝒫 𝑋
40	39	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋)
41	38, 40	eleqtrd 2862	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ∈ 𝒫 𝑋)
42		elpwi 4563	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
43	41, 42	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ⊆ 𝑋)
44	43	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑦 ⊆ 𝑋)
45	37, 44	sstrd 3918	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ⊆ 𝑋)
46		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ∈ 𝒫 𝑦)
47		elpwg 4559	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝒫 𝑦 → (𝑧 ∈ 𝒫 𝑋 ↔ 𝑧 ⊆ 𝑋))
48	46, 47	syl 18	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑧 ∈ 𝒫 𝑋 ↔ 𝑧 ⊆ 𝑋))
49	45, 48	mpbird 260	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ∈ 𝒫 𝑋)
50	11	a1i 11	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 0 ∈ ℝ)
51	8, 35, 49, 50	fvmptd3 7018	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑂‘𝑧) = 0)
52	8	fvmpt2 7006	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ 0 ∈ ℝ) → (𝑂‘𝑦) = 0)
53	41, 11, 52	sylancl 598	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → (𝑂‘𝑦) = 0)
54	53	adantr 486	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑂‘𝑦) = 0)
55	51, 54	breq12d 5115	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → ((𝑂‘𝑧) ≤ (𝑂‘𝑦) ↔ 0 ≤ 0))
56	34, 55	mpbird 260	. . . . . . 7 ⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑂‘𝑧) ≤ (𝑂‘𝑦))
57	56	ralrimiva 3154	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → ∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))
58	57	rgen 3078	. . . . 5 ⊢ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)
59	32, 58	pm3.2i 476	. . . 4 ⊢ (((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))
60	33	a1i 11	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 0 ≤ 0)
61	35	cbvmptv 5208	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 𝑋 ↦ 0) = (𝑧 ∈ 𝒫 𝑋 ↦ 0)
62	8, 61	eqtri 2783	. . . . . . . . . 10 ⊢ 𝑂 = (𝑧 ∈ 𝒫 𝑋 ↦ 0)
63	62	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑂 = (𝑧 ∈ 𝒫 𝑋 ↦ 0))
64		eqidd 2761	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝒫 dom 𝑂 ∧ 𝑧 = ∪ 𝑦) → 0 = 0)
65		id 23	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ∈ 𝒫 dom 𝑂)
66	15	pweqi 4572	. . . . . . . . . . . . . 14 ⊢ 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋)
68	65, 67	eleqtrd 2862	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ∈ 𝒫 𝒫 𝑋)
69		elpwi 4563	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝒫 𝒫 𝑋 → 𝑦 ⊆ 𝒫 𝑋)
70	68, 69	syl 18	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ⊆ 𝒫 𝑋)
71		sspwuni 5059	. . . . . . . . . . 11 ⊢ (𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋)
72	70, 71	sylib 221	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦 ⊆ 𝑋)
73		vuniex 7757	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ V
74	73	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦 ∈ V)
75		elpwg 4559	. . . . . . . . . . 11 ⊢ (∪ 𝑦 ∈ V → (∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋))
76	74, 75	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋))
77	72, 76	mpbird 260	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦 ∈ 𝒫 𝑋)
78	11	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 0 ∈ ℝ)
79	63, 64, 77, 78	fvmptd 7002	. . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂‘∪ 𝑦) = 0)
80	63	reseq1d 5968	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂 ↾ 𝑦) = ((𝑧 ∈ 𝒫 𝑋 ↦ 0) ↾ 𝑦))
81		resmpt 6028	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝒫 𝑋 → ((𝑧 ∈ 𝒫 𝑋 ↦ 0) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ 0))
82	70, 81	syl 18	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ((𝑧 ∈ 𝒫 𝑋 ↦ 0) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ 0))
83	80, 82	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂 ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ 0))
84	83	fveq2d 6890	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (Σ^{^}‘(𝑂 ↾ 𝑦)) = (Σ^{^}‘(𝑧 ∈ 𝑦 ↦ 0)))
85		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑧 𝑦 ∈ 𝒫 dom 𝑂
86	85, 65	sge0z 47479	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (Σ^{^}‘(𝑧 ∈ 𝑦 ↦ 0)) = 0)
87	84, 86	eqtrd 2795	. . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (Σ^{^}‘(𝑂 ↾ 𝑦)) = 0)
88	79, 87	breq12d 5115	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ((𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦)) ↔ 0 ≤ 0))
89	60, 88	mpbird 260	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦)))
90	89	a1d 26	. . . . 5 ⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦))))
91	90	rgen 3078	. . . 4 ⊢ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦)))
92	59, 91	pm3.2i 476	. . 3 ⊢ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦))))
93	92	a1i 11	. 2 ⊢ (𝜑 → ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦)))))
94	8	a1i 11	. . . 4 ⊢ (𝜑 → 𝑂 = (𝑦 ∈ 𝒫 𝑋 ↦ 0))
95		0ome.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
96	95	pwexd 5340	. . . . 5 ⊢ (𝜑 → 𝒫 𝑋 ∈ V)
97		mptexg 7228	. . . . 5 ⊢ (𝒫 𝑋 ∈ V → (𝑦 ∈ 𝒫 𝑋 ↦ 0) ∈ V)
98	96, 97	syl 18	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝒫 𝑋 ↦ 0) ∈ V)
99	94, 98	eqeltrd 2860	. . 3 ⊢ (𝜑 → 𝑂 ∈ V)
100		isome 47598	. . 3 ⊢ (𝑂 ∈ V → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦))))))
101	99, 100	syl 18	. 2 ⊢ (𝜑 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^{^}‘(𝑂 ↾ 𝑦))))))
102	93, 101	mpbird 260	1 ⊢ (𝜑 → 𝑂 ∈ OutMeas)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 Vcvv 3450 ⊆ wss 3895 ∅c0 4278 𝒫 cpw 4556 ∪ cuni 4866 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ↾ cres 5652 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ωcom 7878 ≼ cdom 8975 ℝcr 11203 0cc0 11204 +∞cpnf 11344 ≤ cle 11348 [,]cicc 13483 Σ^{^}csumge0 47466 OutMeascome 47593

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-oi 9508 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-n0 12611 df-z 12698 df-uz 12970 df-rp 13125 df-ico 13486 df-icc 13487 df-fz 13644 df-fzo 13793 df-seq 14149 df-exp 14209 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-clim 15661 df-sum 15860 df-sumge0 47467 df-ome 47594

This theorem is used by: (None)

W3C validator