Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovoliunnfl Structured version   Visualization version   GIF version

Theorem ovoliunnfl 34926
 Description: ovoliun 24098 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.)
Hypothesis
Ref Expression
ovoliunnfl.0 ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) ∈ ℝ)) → (vol*‘ 𝑚 ∈ ℕ (𝑓𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ))
Assertion
Ref Expression
ovoliunnfl ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Distinct variable group:   𝑓,𝑛,𝑚,𝑥,𝐴

Proof of Theorem ovoliunnfl
Dummy variable 𝑙 is distinct from all other variables.
StepHypRef Expression
1 unieq 4838 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4857 . . . . . . . . 9 ∅ = ∅
31, 2syl6eq 2870 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6667 . . . . . . 7 (𝐴 = ∅ → (vol*‘ 𝐴) = (vol*‘∅))
5 ovol0 24086 . . . . . . 7 (vol*‘∅) = 0
64, 5syl6req 2871 . . . . . 6 (𝐴 = ∅ → 0 = (vol*‘ 𝐴))
76a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol*‘ 𝐴)))
8 ovolge0 24074 . . . . . . . 8 ( 𝐴 ⊆ ℝ → 0 ≤ (vol*‘ 𝐴))
98ad2antll 727 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 ≤ (vol*‘ 𝐴))
10 reldom 8507 . . . . . . . . . . . 12 Rel ≼
1110brrelex1i 5601 . . . . . . . . . . 11 (𝐴 ≼ ℕ → 𝐴 ∈ V)
12 0sdomg 8638 . . . . . . . . . . 11 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1311, 12syl 17 . . . . . . . . . 10 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1413biimparc 482 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
15 fodomr 8660 . . . . . . . . 9 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑓 𝑓:ℕ–onto𝐴)
1614, 15sylancom 590 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑓 𝑓:ℕ–onto𝐴)
17 unissb 4861 . . . . . . . . . . . 12 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
1817anbi1i 625 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
19 r19.26 3168 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2018, 19bitr4i 280 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
21 brdom2 8531 . . . . . . . . . . . . . 14 (𝑥 ≼ ℕ ↔ (𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ))
22 nnenom 13340 . . . . . . . . . . . . . . . . 17 ℕ ≈ ω
23 sdomen2 8654 . . . . . . . . . . . . . . . . 17 (ℕ ≈ ω → (𝑥 ≺ ℕ ↔ 𝑥 ≺ ω))
2422, 23ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑥 ≺ ℕ ↔ 𝑥 ≺ ω)
25 isfinite 9107 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
2624, 25bitr4i 280 . . . . . . . . . . . . . . 15 (𝑥 ≺ ℕ ↔ 𝑥 ∈ Fin)
2726orbi1i 910 . . . . . . . . . . . . . 14 ((𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ) ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ))
2821, 27bitri 277 . . . . . . . . . . . . 13 (𝑥 ≼ ℕ ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ))
29 ovolfi 24087 . . . . . . . . . . . . . . 15 ((𝑥 ∈ Fin ∧ 𝑥 ⊆ ℝ) → (vol*‘𝑥) = 0)
3029expcom 416 . . . . . . . . . . . . . 14 (𝑥 ⊆ ℝ → (𝑥 ∈ Fin → (vol*‘𝑥) = 0))
31 ovolctb 24083 . . . . . . . . . . . . . . 15 ((𝑥 ⊆ ℝ ∧ 𝑥 ≈ ℕ) → (vol*‘𝑥) = 0)
3231ex 415 . . . . . . . . . . . . . 14 (𝑥 ⊆ ℝ → (𝑥 ≈ ℕ → (vol*‘𝑥) = 0))
3330, 32jaod 855 . . . . . . . . . . . . 13 (𝑥 ⊆ ℝ → ((𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ) → (vol*‘𝑥) = 0))
3428, 33syl5bi 244 . . . . . . . . . . . 12 (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
3534imdistani 571 . . . . . . . . . . 11 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
3635ralimi 3158 . . . . . . . . . 10 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
3720, 36sylbi 219 . . . . . . . . 9 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
3837ancoms 461 . . . . . . . 8 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
39 foima 6588 . . . . . . . . . . . . 13 (𝑓:ℕ–onto𝐴 → (𝑓 “ ℕ) = 𝐴)
4039raleqdv 3414 . . . . . . . . . . . 12 (𝑓:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
41 fofn 6585 . . . . . . . . . . . . 13 (𝑓:ℕ–onto𝐴𝑓 Fn ℕ)
42 ssid 3987 . . . . . . . . . . . . 13 ℕ ⊆ ℕ
43 sseq1 3990 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓𝑙) → (𝑥 ⊆ ℝ ↔ (𝑓𝑙) ⊆ ℝ))
44 fveqeq2 6672 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓𝑙) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑓𝑙)) = 0))
4543, 44anbi12d 632 . . . . . . . . . . . . . 14 (𝑥 = (𝑓𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)))
4645ralima 6992 . . . . . . . . . . . . 13 ((𝑓 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)))
4741, 42, 46sylancl 588 . . . . . . . . . . . 12 (𝑓:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)))
4840, 47bitr3d 283 . . . . . . . . . . 11 (𝑓:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)))
49 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑛 → (𝑓𝑙) = (𝑓𝑛))
5049sseq1d 3996 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑛 → ((𝑓𝑙) ⊆ ℝ ↔ (𝑓𝑛) ⊆ ℝ))
51 2fveq3 6668 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑛 → (vol*‘(𝑓𝑙)) = (vol*‘(𝑓𝑛)))
5251eqeq1d 2821 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑛 → ((vol*‘(𝑓𝑙)) = 0 ↔ (vol*‘(𝑓𝑛)) = 0))
5350, 52anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑛 → (((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) ↔ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) = 0)))
5453cbvralvw 3448 . . . . . . . . . . . . . . 15 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) ↔ ∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) = 0))
55 0re 10635 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
56 eleq1a 2906 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((vol*‘(𝑓𝑛)) = 0 → (vol*‘(𝑓𝑛)) ∈ ℝ))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . 17 ((vol*‘(𝑓𝑛)) = 0 → (vol*‘(𝑓𝑛)) ∈ ℝ)
5857anim2i 618 . . . . . . . . . . . . . . . 16 (((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) = 0) → ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) ∈ ℝ))
5958ralimi 3158 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) = 0) → ∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) ∈ ℝ))
6054, 59sylbi 219 . . . . . . . . . . . . . 14 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → ∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) ∈ ℝ))
61 ovoliunnfl.0 . . . . . . . . . . . . . 14 ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓𝑛) ⊆ ℝ ∧ (vol*‘(𝑓𝑛)) ∈ ℝ)) → (vol*‘ 𝑚 ∈ ℕ (𝑓𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ))
6241, 60, 61syl2an 597 . . . . . . . . . . . . 13 ((𝑓:ℕ–onto𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)) → (vol*‘ 𝑚 ∈ ℕ (𝑓𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ))
63 fofun 6584 . . . . . . . . . . . . . . . . 17 (𝑓:ℕ–onto𝐴 → Fun 𝑓)
64 funiunfv 6999 . . . . . . . . . . . . . . . . 17 (Fun 𝑓 𝑚 ∈ ℕ (𝑓𝑚) = (𝑓 “ ℕ))
6563, 64syl 17 . . . . . . . . . . . . . . . 16 (𝑓:ℕ–onto𝐴 𝑚 ∈ ℕ (𝑓𝑚) = (𝑓 “ ℕ))
6639unieqd 4840 . . . . . . . . . . . . . . . 16 (𝑓:ℕ–onto𝐴 (𝑓 “ ℕ) = 𝐴)
6765, 66eqtrd 2854 . . . . . . . . . . . . . . 15 (𝑓:ℕ–onto𝐴 𝑚 ∈ ℕ (𝑓𝑚) = 𝐴)
6867fveq2d 6667 . . . . . . . . . . . . . 14 (𝑓:ℕ–onto𝐴 → (vol*‘ 𝑚 ∈ ℕ (𝑓𝑚)) = (vol*‘ 𝐴))
6968adantr 483 . . . . . . . . . . . . 13 ((𝑓:ℕ–onto𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)) → (vol*‘ 𝑚 ∈ ℕ (𝑓𝑚)) = (vol*‘ 𝐴))
70 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑚 → (𝑓𝑙) = (𝑓𝑚))
7170sseq1d 3996 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑚 → ((𝑓𝑙) ⊆ ℝ ↔ (𝑓𝑚) ⊆ ℝ))
72 2fveq3 6668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑚 → (vol*‘(𝑓𝑙)) = (vol*‘(𝑓𝑚)))
7372eqeq1d 2821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑚 → ((vol*‘(𝑓𝑙)) = 0 ↔ (vol*‘(𝑓𝑚)) = 0))
7471, 73anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑚 → (((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) ↔ ((𝑓𝑚) ⊆ ℝ ∧ (vol*‘(𝑓𝑚)) = 0)))
7574rspccva 3620 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → ((𝑓𝑚) ⊆ ℝ ∧ (vol*‘(𝑓𝑚)) = 0))
7675simprd 498 . . . . . . . . . . . . . . . . . . 19 ((∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑓𝑚)) = 0)
7776mpteq2dva 5152 . . . . . . . . . . . . . . . . . 18 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚))) = (𝑚 ∈ ℕ ↦ 0))
7877seqeq3d 13369 . . . . . . . . . . . . . . . . 17 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦ 0)))
7978rneqd 5801 . . . . . . . . . . . . . . . 16 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))) = ran seq1( + , (𝑚 ∈ ℕ ↦ 0)))
8079supeq1d 8902 . . . . . . . . . . . . . . 15 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ) = sup(ran seq1( + , (𝑚 ∈ ℕ ↦ 0)), ℝ*, < ))
81 0cn 10625 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℂ
82 ser1const 13418 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℂ ∧ 𝑙 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑙) = (𝑙 · 0))
8381, 82mpan 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑙) = (𝑙 · 0))
84 nncn 11638 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ ℕ → 𝑙 ∈ ℂ)
8584mul01d 10831 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 ∈ ℕ → (𝑙 · 0) = 0)
8683, 85eqtrd 2854 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑙) = 0)
8786mpteq2ia 5148 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙)) = (𝑙 ∈ ℕ ↦ 0)
88 fconstmpt 5607 . . . . . . . . . . . . . . . . . . . . . 22 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
89 seqeq3 13366 . . . . . . . . . . . . . . . . . . . . . 22 ((ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦ 0)))
9088, 89ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 seq1( + , (ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦ 0))
91 1z 12004 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℤ
92 seqfn 13373 . . . . . . . . . . . . . . . . . . . . . . 23 (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ‘1))
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 seq1( + , (ℕ × {0})) Fn (ℤ‘1)
94 nnuz 12273 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℤ‘1)
9594fneq2i 6444 . . . . . . . . . . . . . . . . . . . . . . 23 (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ‘1))
96 dffn5 6717 . . . . . . . . . . . . . . . . . . . . . . 23 (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) = (𝑙 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙)))
9795, 96bitr3i 279 . . . . . . . . . . . . . . . . . . . . . 22 (seq1( + , (ℕ × {0})) Fn (ℤ‘1) ↔ seq1( + , (ℕ × {0})) = (𝑙 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙)))
9893, 97mpbi 232 . . . . . . . . . . . . . . . . . . . . 21 seq1( + , (ℕ × {0})) = (𝑙 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙))
9990, 98eqtr3i 2844 . . . . . . . . . . . . . . . . . . . 20 seq1( + , (𝑚 ∈ ℕ ↦ 0)) = (𝑙 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙))
100 fconstmpt 5607 . . . . . . . . . . . . . . . . . . . 20 (ℕ × {0}) = (𝑙 ∈ ℕ ↦ 0)
10187, 99, 1003eqtr4i 2852 . . . . . . . . . . . . . . . . . . 19 seq1( + , (𝑚 ∈ ℕ ↦ 0)) = (ℕ × {0})
102101rneqi 5800 . . . . . . . . . . . . . . . . . 18 ran seq1( + , (𝑚 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
103 1nn 11641 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℕ
104 ne0i 4298 . . . . . . . . . . . . . . . . . . 19 (1 ∈ ℕ → ℕ ≠ ∅)
105 rnxp 6020 . . . . . . . . . . . . . . . . . . 19 (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
106103, 104, 105mp2b 10 . . . . . . . . . . . . . . . . . 18 ran (ℕ × {0}) = {0}
107102, 106eqtri 2842 . . . . . . . . . . . . . . . . 17 ran seq1( + , (𝑚 ∈ ℕ ↦ 0)) = {0}
108107supeq1i 8903 . . . . . . . . . . . . . . . 16 sup(ran seq1( + , (𝑚 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
109 xrltso 12526 . . . . . . . . . . . . . . . . 17 < Or ℝ*
110 0xr 10680 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
111 supsn 8928 . . . . . . . . . . . . . . . . 17 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
112109, 110, 111mp2an 690 . . . . . . . . . . . . . . . 16 sup({0}, ℝ*, < ) = 0
113108, 112eqtri 2842 . . . . . . . . . . . . . . 15 sup(ran seq1( + , (𝑚 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
11480, 113syl6eq 2870 . . . . . . . . . . . . . 14 (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ) = 0)
115114adantl 484 . . . . . . . . . . . . 13 ((𝑓:ℕ–onto𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)) → sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓𝑚)))), ℝ*, < ) = 0)
11662, 69, 1153brtr3d 5088 . . . . . . . . . . . 12 ((𝑓:ℕ–onto𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0)) → (vol*‘ 𝐴) ≤ 0)
117116ex 415 . . . . . . . . . . 11 (𝑓:ℕ–onto𝐴 → (∀𝑙 ∈ ℕ ((𝑓𝑙) ⊆ ℝ ∧ (vol*‘(𝑓𝑙)) = 0) → (vol*‘ 𝐴) ≤ 0))
11848, 117sylbid 242 . . . . . . . . . 10 (𝑓:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘ 𝐴) ≤ 0))
119118exlimiv 1925 . . . . . . . . 9 (∃𝑓 𝑓:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘ 𝐴) ≤ 0))
120119imp 409 . . . . . . . 8 ((∃𝑓 𝑓:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) → (vol*‘ 𝐴) ≤ 0)
12116, 38, 120syl2an 597 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → (vol*‘ 𝐴) ≤ 0)
122 ovolcl 24071 . . . . . . . . 9 ( 𝐴 ⊆ ℝ → (vol*‘ 𝐴) ∈ ℝ*)
123 xrletri3 12539 . . . . . . . . 9 ((0 ∈ ℝ* ∧ (vol*‘ 𝐴) ∈ ℝ*) → (0 = (vol*‘ 𝐴) ↔ (0 ≤ (vol*‘ 𝐴) ∧ (vol*‘ 𝐴) ≤ 0)))
124110, 122, 123sylancr 589 . . . . . . . 8 ( 𝐴 ⊆ ℝ → (0 = (vol*‘ 𝐴) ↔ (0 ≤ (vol*‘ 𝐴) ∧ (vol*‘ 𝐴) ≤ 0)))
125124ad2antll 727 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → (0 = (vol*‘ 𝐴) ↔ (0 ≤ (vol*‘ 𝐴) ∧ (vol*‘ 𝐴) ≤ 0)))
1269, 121, 125mpbir2and 711 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol*‘ 𝐴))
127126expl 460 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol*‘ 𝐴)))
1287, 127pm2.61ine 3098 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol*‘ 𝐴))
129 renepnf 10681 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
13055, 129mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
131 fveq2 6663 . . . . . . 7 ( 𝐴 = ℝ → (vol*‘ 𝐴) = (vol*‘ℝ))
132 ovolre 24118 . . . . . . 7 (vol*‘ℝ) = +∞
133131, 132syl6eq 2870 . . . . . 6 ( 𝐴 = ℝ → (vol*‘ 𝐴) = +∞)
134130, 133neeqtrrd 3088 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol*‘ 𝐴))
135134necon2i 3048 . . . 4 (0 = (vol*‘ 𝐴) → 𝐴 ≠ ℝ)
136128, 135syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
137136expr 459 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
138 eqimss 4021 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
139138necon3bi 3040 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
140137, 139pm2.61d1 182 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1531  ∃wex 1774   ∈ wcel 2108   ≠ wne 3014  ∀wral 3136  Vcvv 3493   ⊆ wss 3934  ∅c0 4289  {csn 4559  ∪ cuni 4830  ∪ ciun 4910   class class class wbr 5057   ↦ cmpt 5137   Or wor 5466   × cxp 5546  ran crn 5549   “ cima 5551  Fun wfun 6342   Fn wfn 6343  –onto→wfo 6346  ‘cfv 6348  (class class class)co 7148  ωcom 7572   ≈ cen 8498   ≼ cdom 8499   ≺ csdm 8500  Fincfn 8501  supcsup 8896  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  +∞cpnf 10664  ℝ*cxr 10666   < clt 10667   ≤ cle 10668  ℕcn 11630  ℤcz 11973  ℤ≥cuz 12235  seqcseq 13361  vol*covol 24055 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-fal 1544  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12885  df-fzo 13026  df-seq 13362  df-exp 13422  df-hash 13683  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-rest 16688  df-topgen 16709  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-top 21494  df-topon 21511  df-bases 21546  df-cmp 21987  df-ovol 24057 This theorem is referenced by:  ex-ovoliunnfl  34927
 Copyright terms: Public domain W3C validator