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

Theorem ovnsubadd2lem 46601
Description: (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovnsubadd2lem.x (𝜑𝑋 ∈ Fin)
ovnsubadd2lem.a (𝜑𝐴 ⊆ (ℝ ↑m 𝑋))
ovnsubadd2lem.b (𝜑𝐵 ⊆ (ℝ ↑m 𝑋))
ovnsubadd2lem.c 𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
Assertion
Ref Expression
ovnsubadd2lem (𝜑 → ((voln*‘𝑋)‘(𝐴𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝐶,𝑛   𝑛,𝑋   𝜑,𝑛

Proof of Theorem ovnsubadd2lem
StepHypRef Expression
1 ovnsubadd2lem.x . . 3 (𝜑𝑋 ∈ Fin)
2 iftrue 4537 . . . . . . . 8 (𝑛 = 1 → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐴)
32adantl 481 . . . . . . 7 ((𝜑𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐴)
4 ovexd 7466 . . . . . . . . . 10 (𝜑 → (ℝ ↑m 𝑋) ∈ V)
5 ovnsubadd2lem.a . . . . . . . . . 10 (𝜑𝐴 ⊆ (ℝ ↑m 𝑋))
64, 5ssexd 5330 . . . . . . . . 9 (𝜑𝐴 ∈ V)
76, 5elpwd 4611 . . . . . . . 8 (𝜑𝐴 ∈ 𝒫 (ℝ ↑m 𝑋))
87adantr 480 . . . . . . 7 ((𝜑𝑛 = 1) → 𝐴 ∈ 𝒫 (ℝ ↑m 𝑋))
93, 8eqeltrd 2839 . . . . . 6 ((𝜑𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
109adantlr 715 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
11 simpl 482 . . . . . . . . . . 11 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → ¬ 𝑛 = 1)
1211iffalsed 4542 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = if(𝑛 = 2, 𝐵, ∅))
13 simpr 484 . . . . . . . . . . 11 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → 𝑛 = 2)
1413iftrued 4539 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → if(𝑛 = 2, 𝐵, ∅) = 𝐵)
1512, 14eqtrd 2775 . . . . . . . . 9 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
1615adantll 714 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
17 ovnsubadd2lem.b . . . . . . . . . . 11 (𝜑𝐵 ⊆ (ℝ ↑m 𝑋))
184, 17ssexd 5330 . . . . . . . . . 10 (𝜑𝐵 ∈ V)
1918, 17elpwd 4611 . . . . . . . . 9 (𝜑𝐵 ∈ 𝒫 (ℝ ↑m 𝑋))
2019ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → 𝐵 ∈ 𝒫 (ℝ ↑m 𝑋))
2116, 20eqeltrd 2839 . . . . . . 7 (((𝜑 ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
2221adantllr 719 . . . . . 6 ((((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
23 simpl 482 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → ¬ 𝑛 = 1)
2423iffalsed 4542 . . . . . . . . 9 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = if(𝑛 = 2, 𝐵, ∅))
25 simpr 484 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → ¬ 𝑛 = 2)
2625iffalsed 4542 . . . . . . . . 9 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 2, 𝐵, ∅) = ∅)
2724, 26eqtrd 2775 . . . . . . . 8 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = ∅)
28 0elpw 5362 . . . . . . . . 9 ∅ ∈ 𝒫 (ℝ ↑m 𝑋)
2928a1i 11 . . . . . . . 8 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → ∅ ∈ 𝒫 (ℝ ↑m 𝑋))
3027, 29eqeltrd 2839 . . . . . . 7 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
3130adantll 714 . . . . . 6 ((((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛 = 1) ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
3222, 31pm2.61dan 813 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
3310, 32pm2.61dan 813 . . . 4 ((𝜑𝑛 ∈ ℕ) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑m 𝑋))
34 ovnsubadd2lem.c . . . 4 𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
3533, 34fmptd 7134 . . 3 (𝜑𝐶:ℕ⟶𝒫 (ℝ ↑m 𝑋))
361, 35ovnsubadd 46528 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐶𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))))
37 eldifi 4141 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ {1, 2}) → 𝑛 ∈ ℕ)
3837adantl 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → 𝑛 ∈ ℕ)
39 eldifn 4142 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ {1, 2}) → ¬ 𝑛 ∈ {1, 2})
40 vex 3482 . . . . . . . . . . . . . . . . 17 𝑛 ∈ V
4140a1i 11 . . . . . . . . . . . . . . . 16 𝑛 ∈ {1, 2} → 𝑛 ∈ V)
42 id 22 . . . . . . . . . . . . . . . 16 𝑛 ∈ {1, 2} → ¬ 𝑛 ∈ {1, 2})
4341, 42nelpr1 4659 . . . . . . . . . . . . . . 15 𝑛 ∈ {1, 2} → 𝑛 ≠ 1)
4443neneqd 2943 . . . . . . . . . . . . . 14 𝑛 ∈ {1, 2} → ¬ 𝑛 = 1)
4539, 44syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ {1, 2}) → ¬ 𝑛 = 1)
4641, 42nelpr2 4658 . . . . . . . . . . . . . . 15 𝑛 ∈ {1, 2} → 𝑛 ≠ 2)
4746neneqd 2943 . . . . . . . . . . . . . 14 𝑛 ∈ {1, 2} → ¬ 𝑛 = 2)
4839, 47syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ {1, 2}) → ¬ 𝑛 = 2)
4945, 48, 27syl2anc 584 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ {1, 2}) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = ∅)
50 0ex 5313 . . . . . . . . . . . . 13 ∅ ∈ V
5150a1i 11 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ {1, 2}) → ∅ ∈ V)
5249, 51eqeltrd 2839 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ {1, 2}) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ V)
5352adantl 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ V)
5434fvmpt2 7027 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ V) → (𝐶𝑛) = if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
5538, 53, 54syl2anc 584 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → (𝐶𝑛) = if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
5649adantl 481 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = ∅)
5755, 56eqtrd 2775 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → (𝐶𝑛) = ∅)
5857ralrimiva 3144 . . . . . . 7 (𝜑 → ∀𝑛 ∈ (ℕ ∖ {1, 2})(𝐶𝑛) = ∅)
59 nfcv 2903 . . . . . . . 8 𝑛(ℕ ∖ {1, 2})
6059iunxdif3 5100 . . . . . . 7 (∀𝑛 ∈ (ℕ ∖ {1, 2})(𝐶𝑛) = ∅ → 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ ℕ (𝐶𝑛))
6158, 60syl 17 . . . . . 6 (𝜑 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ ℕ (𝐶𝑛))
6261eqcomd 2741 . . . . 5 (𝜑 𝑛 ∈ ℕ (𝐶𝑛) = 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛))
63 1nn 12275 . . . . . . . . . 10 1 ∈ ℕ
64 2nn 12337 . . . . . . . . . 10 2 ∈ ℕ
6563, 64pm3.2i 470 . . . . . . . . 9 (1 ∈ ℕ ∧ 2 ∈ ℕ)
66 prssi 4826 . . . . . . . . 9 ((1 ∈ ℕ ∧ 2 ∈ ℕ) → {1, 2} ⊆ ℕ)
6765, 66ax-mp 5 . . . . . . . 8 {1, 2} ⊆ ℕ
68 dfss4 4275 . . . . . . . 8 ({1, 2} ⊆ ℕ ↔ (ℕ ∖ (ℕ ∖ {1, 2})) = {1, 2})
6967, 68mpbi 230 . . . . . . 7 (ℕ ∖ (ℕ ∖ {1, 2})) = {1, 2}
70 iuneq1 5013 . . . . . . 7 ((ℕ ∖ (ℕ ∖ {1, 2})) = {1, 2} → 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ {1, 2} (𝐶𝑛))
7169, 70ax-mp 5 . . . . . 6 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ {1, 2} (𝐶𝑛)
7271a1i 11 . . . . 5 (𝜑 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ {1, 2} (𝐶𝑛))
73 fveq2 6907 . . . . . . . . 9 (𝑛 = 1 → (𝐶𝑛) = (𝐶‘1))
74 fveq2 6907 . . . . . . . . 9 (𝑛 = 2 → (𝐶𝑛) = (𝐶‘2))
7573, 74iunxprg 5101 . . . . . . . 8 ((1 ∈ ℕ ∧ 2 ∈ ℕ) → 𝑛 ∈ {1, 2} (𝐶𝑛) = ((𝐶‘1) ∪ (𝐶‘2)))
7663, 64, 75mp2an 692 . . . . . . 7 𝑛 ∈ {1, 2} (𝐶𝑛) = ((𝐶‘1) ∪ (𝐶‘2))
7776a1i 11 . . . . . 6 (𝜑 𝑛 ∈ {1, 2} (𝐶𝑛) = ((𝐶‘1) ∪ (𝐶‘2)))
7863a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℕ)
7934, 2, 78, 6fvmptd3 7039 . . . . . . 7 (𝜑 → (𝐶‘1) = 𝐴)
80 id 22 . . . . . . . . . . . 12 (𝑛 = 2 → 𝑛 = 2)
81 1ne2 12472 . . . . . . . . . . . . . 14 1 ≠ 2
8281necomi 2993 . . . . . . . . . . . . 13 2 ≠ 1
8382a1i 11 . . . . . . . . . . . 12 (𝑛 = 2 → 2 ≠ 1)
8480, 83eqnetrd 3006 . . . . . . . . . . 11 (𝑛 = 2 → 𝑛 ≠ 1)
8584neneqd 2943 . . . . . . . . . 10 (𝑛 = 2 → ¬ 𝑛 = 1)
8685iffalsed 4542 . . . . . . . . 9 (𝑛 = 2 → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = if(𝑛 = 2, 𝐵, ∅))
87 iftrue 4537 . . . . . . . . 9 (𝑛 = 2 → if(𝑛 = 2, 𝐵, ∅) = 𝐵)
8886, 87eqtrd 2775 . . . . . . . 8 (𝑛 = 2 → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
8964a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
9034, 88, 89, 18fvmptd3 7039 . . . . . . 7 (𝜑 → (𝐶‘2) = 𝐵)
9179, 90uneq12d 4179 . . . . . 6 (𝜑 → ((𝐶‘1) ∪ (𝐶‘2)) = (𝐴𝐵))
92 eqidd 2736 . . . . . 6 (𝜑 → (𝐴𝐵) = (𝐴𝐵))
9377, 91, 923eqtrd 2779 . . . . 5 (𝜑 𝑛 ∈ {1, 2} (𝐶𝑛) = (𝐴𝐵))
9462, 72, 933eqtrd 2779 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐶𝑛) = (𝐴𝐵))
9594fveq2d 6911 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐶𝑛)) = ((voln*‘𝑋)‘(𝐴𝐵)))
96 nfv 1912 . . . . . 6 𝑛𝜑
97 nnex 12270 . . . . . . 7 ℕ ∈ V
9897a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
9967a1i 11 . . . . . 6 (𝜑 → {1, 2} ⊆ ℕ)
1001adantr 480 . . . . . . 7 ((𝜑𝑛 ∈ {1, 2}) → 𝑋 ∈ Fin)
101 simpl 482 . . . . . . . 8 ((𝜑𝑛 ∈ {1, 2}) → 𝜑)
10299sselda 3995 . . . . . . . 8 ((𝜑𝑛 ∈ {1, 2}) → 𝑛 ∈ ℕ)
10335ffvelcdmda 7104 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛) ∈ 𝒫 (ℝ ↑m 𝑋))
104 elpwi 4612 . . . . . . . . 9 ((𝐶𝑛) ∈ 𝒫 (ℝ ↑m 𝑋) → (𝐶𝑛) ⊆ (ℝ ↑m 𝑋))
105103, 104syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛) ⊆ (ℝ ↑m 𝑋))
106101, 102, 105syl2anc 584 . . . . . . 7 ((𝜑𝑛 ∈ {1, 2}) → (𝐶𝑛) ⊆ (ℝ ↑m 𝑋))
107100, 106ovncl 46523 . . . . . 6 ((𝜑𝑛 ∈ {1, 2}) → ((voln*‘𝑋)‘(𝐶𝑛)) ∈ (0[,]+∞))
10857fveq2d 6911 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → ((voln*‘𝑋)‘(𝐶𝑛)) = ((voln*‘𝑋)‘∅))
1091adantr 480 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → 𝑋 ∈ Fin)
110109ovn0 46522 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → ((voln*‘𝑋)‘∅) = 0)
111108, 110eqtrd 2775 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → ((voln*‘𝑋)‘(𝐶𝑛)) = 0)
11296, 98, 99, 107, 111sge0ss 46368 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ {1, 2} ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))))
113112eqcomd 2741 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (Σ^‘(𝑛 ∈ {1, 2} ↦ ((voln*‘𝑋)‘(𝐶𝑛)))))
11479, 5eqsstrd 4034 . . . . . 6 (𝜑 → (𝐶‘1) ⊆ (ℝ ↑m 𝑋))
1151, 114ovncl 46523 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘1)) ∈ (0[,]+∞))
11690, 17eqsstrd 4034 . . . . . 6 (𝜑 → (𝐶‘2) ⊆ (ℝ ↑m 𝑋))
1171, 116ovncl 46523 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘2)) ∈ (0[,]+∞))
118 2fveq3 6912 . . . . 5 (𝑛 = 1 → ((voln*‘𝑋)‘(𝐶𝑛)) = ((voln*‘𝑋)‘(𝐶‘1)))
119 2fveq3 6912 . . . . 5 (𝑛 = 2 → ((voln*‘𝑋)‘(𝐶𝑛)) = ((voln*‘𝑋)‘(𝐶‘2)))
12081a1i 11 . . . . 5 (𝜑 → 1 ≠ 2)
12178, 89, 115, 117, 118, 119, 120sge0pr 46350 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ {1, 2} ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (((voln*‘𝑋)‘(𝐶‘1)) +𝑒 ((voln*‘𝑋)‘(𝐶‘2))))
12279fveq2d 6911 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘1)) = ((voln*‘𝑋)‘𝐴))
12390fveq2d 6911 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘2)) = ((voln*‘𝑋)‘𝐵))
124122, 123oveq12d 7449 . . . 4 (𝜑 → (((voln*‘𝑋)‘(𝐶‘1)) +𝑒 ((voln*‘𝑋)‘(𝐶‘2))) = (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
125113, 121, 1243eqtrd 2779 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
12695, 125breq12d 5161 . 2 (𝜑 → (((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐶𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) ↔ ((voln*‘𝑋)‘(𝐴𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵))))
12736, 126mpbid 232 1 (𝜑 → ((voln*‘𝑋)‘(𝐴𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1537  wcel 2106  wne 2938  wral 3059  Vcvv 3478  cdif 3960  cun 3961  wss 3963  c0 4339  ifcif 4531  𝒫 cpw 4605  {cpr 4633   ciun 4996   class class class wbr 5148  cmpt 5231  cfv 6563  (class class class)co 7431  m cmap 8865  Fincfn 8984  cr 11152  0cc0 11153  1c1 11154  cle 11294  cn 12264  2c2 12319   +𝑒 cxad 13150  Σ^csumge0 46318  voln*covoln 46492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cc 10473  ax-ac2 10501  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-acn 9980  df-ac 10154  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-rlim 15522  df-sum 15720  df-prod 15937  df-rest 17469  df-topgen 17490  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-top 22916  df-topon 22933  df-bases 22969  df-cmp 23411  df-ovol 25513  df-vol 25514  df-sumge0 46319  df-ovoln 46493
This theorem is referenced by:  ovnsubadd2  46602
  Copyright terms: Public domain W3C validator