MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iccsplit Structured version   Visualization version   GIF version

Theorem iccsplit 12250
Description: Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
iccsplit ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵)))

Proof of Theorem iccsplit
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simplr1 1101 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝑥 < 𝐶) → 𝑥 ∈ ℝ)
2 simplr2 1102 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝑥 < 𝐶) → 𝐴𝑥)
3 simpr1 1065 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) → 𝑥 ∈ ℝ)
4 iccssre 12200 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
54sseld 3583 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) → 𝐶 ∈ ℝ))
653impia 1258 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
76adantr 481 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) → 𝐶 ∈ ℝ)
8 ltle 10073 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑥 < 𝐶𝑥𝐶))
93, 7, 8syl2anc 692 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) → (𝑥 < 𝐶𝑥𝐶))
109imp 445 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝑥 < 𝐶) → 𝑥𝐶)
111, 2, 103jca 1240 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝑥 < 𝐶) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶))
1211orcd 407 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝑥 < 𝐶) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)))
13 simplr1 1101 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝐶𝑥) → 𝑥 ∈ ℝ)
14 simpr 477 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝐶𝑥) → 𝐶𝑥)
15 simplr3 1103 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝐶𝑥) → 𝑥𝐵)
1613, 14, 153jca 1240 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝐶𝑥) → (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵))
1716olcd 408 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) ∧ 𝐶𝑥) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)))
1812, 17, 3, 7ltlecasei 10092 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)))
1918ex 450 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵))))
20 simp1 1059 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝑥 ∈ ℝ)
2120a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝑥 ∈ ℝ))
22 simp2 1060 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝐴𝑥)
2322a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝐴𝑥))
24 elicc2 12183 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵)))
25203ad2ant3 1082 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)) → 𝑥 ∈ ℝ)
26 simp1 1059 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) → 𝐶 ∈ ℝ)
27263ad2ant2 1081 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)) → 𝐶 ∈ ℝ)
28 simp1r 1084 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)) → 𝐵 ∈ ℝ)
29 simp3 1061 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝑥𝐶)
30293ad2ant3 1082 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)) → 𝑥𝐶)
31 simp3 1061 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) → 𝐶𝐵)
32313ad2ant2 1081 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)) → 𝐶𝐵)
3325, 27, 28, 30, 32letrd 10141 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)) → 𝑥𝐵)
34333exp 1261 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝑥𝐵)))
3524, 34sylbid 230 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝑥𝐵)))
36353impia 1258 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → 𝑥𝐵))
3721, 23, 363jcad 1241 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
38 simp1 1059 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝑥 ∈ ℝ)
3938a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝑥 ∈ ℝ))
40 simp1l 1083 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → 𝐴 ∈ ℝ)
41263ad2ant2 1081 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → 𝐶 ∈ ℝ)
42383ad2ant3 1082 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → 𝑥 ∈ ℝ)
43 simp2 1060 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) → 𝐴𝐶)
44433ad2ant2 1081 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → 𝐴𝐶)
45 simp2 1060 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝐶𝑥)
46453ad2ant3 1082 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → 𝐶𝑥)
4740, 41, 42, 44, 46letrd 10141 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) ∧ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → 𝐴𝑥)
48473exp 1261 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵) → ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝐴𝑥)))
4924, 48sylbid 230 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝐴𝑥)))
50493impia 1258 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝐴𝑥))
51 simp3 1061 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝑥𝐵)
5251a1i 11 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → 𝑥𝐵))
5339, 50, 523jcad 1241 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
5437, 53jaod 395 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
5519, 54impbid 202 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵) ↔ ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵))))
56 elicc2 12183 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
57563adant3 1079 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
585imdistani 725 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ))
59583impa 1256 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ))
60 elicc2 12183 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐶) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)))
6160adantlr 750 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐶) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶)))
62 elicc2 12183 . . . . . . . 8 ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐶[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)))
6362ancoms 469 . . . . . . 7 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑥 ∈ (𝐶[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)))
6463adantll 749 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝑥 ∈ (𝐶[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵)))
6561, 64orbi12d 745 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝑥 ∈ (𝐴[,]𝐶) ∨ 𝑥 ∈ (𝐶[,]𝐵)) ↔ ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵))))
6659, 65syl 17 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → ((𝑥 ∈ (𝐴[,]𝐶) ∨ 𝑥 ∈ (𝐶[,]𝐵)) ↔ ((𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐶) ∨ (𝑥 ∈ ℝ ∧ 𝐶𝑥𝑥𝐵))))
6755, 57, 663bitr4d 300 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ (𝐴[,]𝐶) ∨ 𝑥 ∈ (𝐶[,]𝐵))))
68 elun 3733 . . 3 (𝑥 ∈ ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵)) ↔ (𝑥 ∈ (𝐴[,]𝐶) ∨ 𝑥 ∈ (𝐶[,]𝐵)))
6967, 68syl6bbr 278 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑥 ∈ ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵))))
7069eqrdv 2619 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  cun 3554   class class class wbr 4615  (class class class)co 6607  cr 9882   < clt 10021  cle 10022  [,]cicc 12123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-pre-lttri 9957  ax-pre-lttrn 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-po 4997  df-so 4998  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-icc 12127
This theorem is referenced by:  cnmpt2pc  22640  volcn  23287  itgspliticc  23516  cvmliftlem10  31005  iblspltprt  39512
  Copyright terms: Public domain W3C validator