Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carsgclctunlem3 Structured version   Visualization version   GIF version

Theorem carsgclctunlem3 32031
Description: Lemma for carsgclctun 32032. (Contributed by Thierry Arnoux, 24-May-2020.)
Hypotheses
Ref Expression
carsgval.1 (𝜑𝑂𝑉)
carsgval.2 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
carsgsiga.1 (𝜑 → (𝑀‘∅) = 0)
carsgsiga.2 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
carsgsiga.3 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
carsgclctun.1 (𝜑𝐴 ≼ ω)
carsgclctun.2 (𝜑𝐴 ⊆ (toCaraSiga‘𝑀))
carsgclctunlem3.1 (𝜑𝐸 ∈ 𝒫 𝑂)
Assertion
Ref Expression
carsgclctunlem3 (𝜑 → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐸,𝑦   𝑥,𝑀,𝑦   𝑥,𝑂,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem carsgclctunlem3
Dummy variables 𝑒 𝑓 𝑘 𝑛 𝑧 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iccssxr 13048 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
2 carsgval.2 . . . . . . . 8 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
3 carsgclctunlem3.1 . . . . . . . . 9 (𝜑𝐸 ∈ 𝒫 𝑂)
43elpwincl1 30625 . . . . . . . 8 (𝜑 → (𝐸 𝐴) ∈ 𝒫 𝑂)
52, 4ffvelrnd 6927 . . . . . . 7 (𝜑 → (𝑀‘(𝐸 𝐴)) ∈ (0[,]+∞))
61, 5sselid 3915 . . . . . 6 (𝜑 → (𝑀‘(𝐸 𝐴)) ∈ ℝ*)
73elpwdifcl 30626 . . . . . . . 8 (𝜑 → (𝐸 𝐴) ∈ 𝒫 𝑂)
82, 7ffvelrnd 6927 . . . . . . 7 (𝜑 → (𝑀‘(𝐸 𝐴)) ∈ (0[,]+∞))
91, 8sselid 3915 . . . . . 6 (𝜑 → (𝑀‘(𝐸 𝐴)) ∈ ℝ*)
106, 9xaddcld 12921 . . . . 5 (𝜑 → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ∈ ℝ*)
1110adantr 484 . . . 4 ((𝜑 ∧ (𝑀𝐸) = +∞) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ∈ ℝ*)
12 pnfge 12752 . . . 4 (((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ∈ ℝ* → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ +∞)
1311, 12syl 17 . . 3 ((𝜑 ∧ (𝑀𝐸) = +∞) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ +∞)
14 simpr 488 . . 3 ((𝜑 ∧ (𝑀𝐸) = +∞) → (𝑀𝐸) = +∞)
1513, 14breqtrrd 5098 . 2 ((𝜑 ∧ (𝑀𝐸) = +∞) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
16 unieq 4847 . . . . . . . . . . . . 13 (𝐴 = ∅ → 𝐴 = ∅)
17 uni0 4866 . . . . . . . . . . . . 13 ∅ = ∅
1816, 17eqtrdi 2796 . . . . . . . . . . . 12 (𝐴 = ∅ → 𝐴 = ∅)
1918ineq2d 4144 . . . . . . . . . . 11 (𝐴 = ∅ → (𝐸 𝐴) = (𝐸 ∩ ∅))
20 in0 4323 . . . . . . . . . . 11 (𝐸 ∩ ∅) = ∅
2119, 20eqtrdi 2796 . . . . . . . . . 10 (𝐴 = ∅ → (𝐸 𝐴) = ∅)
2221fveq2d 6743 . . . . . . . . 9 (𝐴 = ∅ → (𝑀‘(𝐸 𝐴)) = (𝑀‘∅))
2318difeq2d 4054 . . . . . . . . . . 11 (𝐴 = ∅ → (𝐸 𝐴) = (𝐸 ∖ ∅))
24 dif0 4304 . . . . . . . . . . 11 (𝐸 ∖ ∅) = 𝐸
2523, 24eqtrdi 2796 . . . . . . . . . 10 (𝐴 = ∅ → (𝐸 𝐴) = 𝐸)
2625fveq2d 6743 . . . . . . . . 9 (𝐴 = ∅ → (𝑀‘(𝐸 𝐴)) = (𝑀𝐸))
2722, 26oveq12d 7253 . . . . . . . 8 (𝐴 = ∅ → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) = ((𝑀‘∅) +𝑒 (𝑀𝐸)))
2827adantl 485 . . . . . . 7 ((𝜑𝐴 = ∅) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) = ((𝑀‘∅) +𝑒 (𝑀𝐸)))
29 carsgsiga.1 . . . . . . . . 9 (𝜑 → (𝑀‘∅) = 0)
3029adantr 484 . . . . . . . 8 ((𝜑𝐴 = ∅) → (𝑀‘∅) = 0)
3130oveq1d 7250 . . . . . . 7 ((𝜑𝐴 = ∅) → ((𝑀‘∅) +𝑒 (𝑀𝐸)) = (0 +𝑒 (𝑀𝐸)))
322, 3ffvelrnd 6927 . . . . . . . . . 10 (𝜑 → (𝑀𝐸) ∈ (0[,]+∞))
331, 32sselid 3915 . . . . . . . . 9 (𝜑 → (𝑀𝐸) ∈ ℝ*)
3433adantr 484 . . . . . . . 8 ((𝜑𝐴 = ∅) → (𝑀𝐸) ∈ ℝ*)
35 xaddid2 12862 . . . . . . . 8 ((𝑀𝐸) ∈ ℝ* → (0 +𝑒 (𝑀𝐸)) = (𝑀𝐸))
3634, 35syl 17 . . . . . . 7 ((𝜑𝐴 = ∅) → (0 +𝑒 (𝑀𝐸)) = (𝑀𝐸))
3728, 31, 363eqtrd 2783 . . . . . 6 ((𝜑𝐴 = ∅) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) = (𝑀𝐸))
3837, 34eqeltrd 2840 . . . . . . 7 ((𝜑𝐴 = ∅) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ∈ ℝ*)
39 xeqlelt 30849 . . . . . . 7 ((((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ∈ ℝ* ∧ (𝑀𝐸) ∈ ℝ*) → (((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) = (𝑀𝐸) ↔ (((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸) ∧ ¬ ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) < (𝑀𝐸))))
4038, 34, 39syl2anc 587 . . . . . 6 ((𝜑𝐴 = ∅) → (((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) = (𝑀𝐸) ↔ (((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸) ∧ ¬ ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) < (𝑀𝐸))))
4137, 40mpbid 235 . . . . 5 ((𝜑𝐴 = ∅) → (((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸) ∧ ¬ ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) < (𝑀𝐸)))
4241simpld 498 . . . 4 ((𝜑𝐴 = ∅) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
4342adantlr 715 . . 3 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 = ∅) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
44 carsgclctun.2 . . . . . . . 8 (𝜑𝐴 ⊆ (toCaraSiga‘𝑀))
45 fvex 6752 . . . . . . . . 9 (toCaraSiga‘𝑀) ∈ V
4645ssex 5231 . . . . . . . 8 (𝐴 ⊆ (toCaraSiga‘𝑀) → 𝐴 ∈ V)
47 0sdomg 8801 . . . . . . . 8 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
4844, 46, 473syl 18 . . . . . . 7 (𝜑 → (∅ ≺ 𝐴𝐴 ≠ ∅))
4948biimpar 481 . . . . . 6 ((𝜑𝐴 ≠ ∅) → ∅ ≺ 𝐴)
5049adantlr 715 . . . . 5 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → ∅ ≺ 𝐴)
51 carsgclctun.1 . . . . . . 7 (𝜑𝐴 ≼ ω)
52 nnenom 13585 . . . . . . . 8 ℕ ≈ ω
5352ensymi 8704 . . . . . . 7 ω ≈ ℕ
54 domentr 8713 . . . . . . 7 ((𝐴 ≼ ω ∧ ω ≈ ℕ) → 𝐴 ≼ ℕ)
5551, 53, 54sylancl 589 . . . . . 6 (𝜑𝐴 ≼ ℕ)
5655ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → 𝐴 ≼ ℕ)
57 fodomr 8823 . . . . 5 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑓 𝑓:ℕ–onto𝐴)
5850, 56, 57syl2anc 587 . . . 4 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto𝐴)
59 fveq2 6739 . . . . . . . . . 10 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
6059iundisj 24477 . . . . . . . . 9 𝑛 ∈ ℕ (𝑓𝑛) = 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘))
61 fofn 6657 . . . . . . . . . . . 12 (𝑓:ℕ–onto𝐴𝑓 Fn ℕ)
62 fniunfv 7082 . . . . . . . . . . . 12 (𝑓 Fn ℕ → 𝑛 ∈ ℕ (𝑓𝑛) = ran 𝑓)
6361, 62syl 17 . . . . . . . . . . 11 (𝑓:ℕ–onto𝐴 𝑛 ∈ ℕ (𝑓𝑛) = ran 𝑓)
64 forn 6658 . . . . . . . . . . . 12 (𝑓:ℕ–onto𝐴 → ran 𝑓 = 𝐴)
6564unieqd 4850 . . . . . . . . . . 11 (𝑓:ℕ–onto𝐴 ran 𝑓 = 𝐴)
6663, 65eqtrd 2779 . . . . . . . . . 10 (𝑓:ℕ–onto𝐴 𝑛 ∈ ℕ (𝑓𝑛) = 𝐴)
6766adantl 485 . . . . . . . . 9 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → 𝑛 ∈ ℕ (𝑓𝑛) = 𝐴)
6860, 67eqtr3id 2794 . . . . . . . 8 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)) = 𝐴)
6968ineq2d 4144 . . . . . . 7 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → (𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘))) = (𝐸 𝐴))
7069fveq2d 6743 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → (𝑀‘(𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)))) = (𝑀‘(𝐸 𝐴)))
7168difeq2d 4054 . . . . . . 7 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → (𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘))) = (𝐸 𝐴))
7271fveq2d 6743 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → (𝑀‘(𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)))) = (𝑀‘(𝐸 𝐴)))
7370, 72oveq12d 7253 . . . . 5 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → ((𝑀‘(𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)))) +𝑒 (𝑀‘(𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘))))) = ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))))
74 carsgval.1 . . . . . . 7 (𝜑𝑂𝑉)
7574ad3antrrr 730 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → 𝑂𝑉)
762ad3antrrr 730 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
7729ad3antrrr 730 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → (𝑀‘∅) = 0)
78 carsgsiga.2 . . . . . . . . 9 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
79783adant1r 1179 . . . . . . . 8 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
80793adant1r 1179 . . . . . . 7 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
81803adant1r 1179 . . . . . 6 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
82 carsgsiga.3 . . . . . . . . 9 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
83823adant1r 1179 . . . . . . . 8 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
84833adant1r 1179 . . . . . . 7 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
85843adant1r 1179 . . . . . 6 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
8659iundisj2 24478 . . . . . . 7 Disj 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘))
8786a1i 11 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → Disj 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)))
8875adantr 484 . . . . . . 7 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑂𝑉)
8976adantr 484 . . . . . . 7 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
9044ad4antr 732 . . . . . . . 8 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ (toCaraSiga‘𝑀))
91 fof 6655 . . . . . . . . . 10 (𝑓:ℕ–onto𝐴𝑓:ℕ⟶𝐴)
9291ad2antlr 727 . . . . . . . . 9 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶𝐴)
93 simpr 488 . . . . . . . . 9 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9492, 93ffvelrnd 6927 . . . . . . . 8 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) ∈ 𝐴)
9590, 94sseldd 3919 . . . . . . 7 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) ∈ (toCaraSiga‘𝑀))
9677adantr 484 . . . . . . . 8 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → (𝑀‘∅) = 0)
97813adant1r 1179 . . . . . . . 8 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
9888, 89, 96, 97carsgsigalem 32026 . . . . . . 7 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑒 ∈ 𝒫 𝑂𝑔 ∈ 𝒫 𝑂) → (𝑀‘(𝑒𝑔)) ≤ ((𝑀𝑒) +𝑒 (𝑀𝑔)))
9991ad3antlr 731 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → 𝑓:ℕ⟶𝐴)
100 fzossnn 13321 . . . . . . . . . . . . 13 (1..^𝑛) ⊆ ℕ
101100a1i 11 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → (1..^𝑛) ⊆ ℕ)
102101sselda 3918 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → 𝑘 ∈ ℕ)
10399, 102ffvelrnd 6927 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → (𝑓𝑘) ∈ 𝐴)
104103ralrimiva 3108 . . . . . . . . 9 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1..^𝑛)(𝑓𝑘) ∈ 𝐴)
105 dfiun2g 4957 . . . . . . . . 9 (∀𝑘 ∈ (1..^𝑛)(𝑓𝑘) ∈ 𝐴 𝑘 ∈ (1..^𝑛)(𝑓𝑘) = {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)})
106104, 105syl 17 . . . . . . . 8 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ (1..^𝑛)(𝑓𝑘) = {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)})
107 eqid 2739 . . . . . . . . . . . 12 (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) = (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘))
108107rnmpt 5842 . . . . . . . . . . 11 ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) = {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)}
109 fzofi 13579 . . . . . . . . . . . 12 (1..^𝑛) ∈ Fin
110 mptfi 9005 . . . . . . . . . . . 12 ((1..^𝑛) ∈ Fin → (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) ∈ Fin)
111 rnfi 8989 . . . . . . . . . . . 12 ((𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) ∈ Fin → ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) ∈ Fin)
112109, 110, 111mp2b 10 . . . . . . . . . . 11 ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) ∈ Fin
113108, 112eqeltrri 2837 . . . . . . . . . 10 {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)} ∈ Fin
114113a1i 11 . . . . . . . . 9 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)} ∈ Fin)
11590adantr 484 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → 𝐴 ⊆ (toCaraSiga‘𝑀))
116115, 103sseldd 3919 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → (𝑓𝑘) ∈ (toCaraSiga‘𝑀))
117116ralrimiva 3108 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1..^𝑛)(𝑓𝑘) ∈ (toCaraSiga‘𝑀))
118107rnmptss 6961 . . . . . . . . . . 11 (∀𝑘 ∈ (1..^𝑛)(𝑓𝑘) ∈ (toCaraSiga‘𝑀) → ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) ⊆ (toCaraSiga‘𝑀))
119117, 118syl 17 . . . . . . . . . 10 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓𝑘)) ⊆ (toCaraSiga‘𝑀))
120108, 119eqsstrrid 3967 . . . . . . . . 9 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)} ⊆ (toCaraSiga‘𝑀))
12188, 89, 96, 97, 114, 120fiunelcarsg 32027 . . . . . . . 8 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓𝑘)} ∈ (toCaraSiga‘𝑀))
122106, 121eqeltrd 2840 . . . . . . 7 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑘 ∈ (1..^𝑛)(𝑓𝑘) ∈ (toCaraSiga‘𝑀))
12388, 89, 95, 98, 122difelcarsg2 32024 . . . . . 6 (((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) ∧ 𝑛 ∈ ℕ) → ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)) ∈ (toCaraSiga‘𝑀))
1243ad3antrrr 730 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → 𝐸 ∈ 𝒫 𝑂)
125 simpllr 776 . . . . . 6 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → (𝑀𝐸) ≠ +∞)
12675, 76, 77, 81, 85, 87, 123, 124, 125carsgclctunlem2 32030 . . . . 5 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → ((𝑀‘(𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘)))) +𝑒 (𝑀‘(𝐸 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑘 ∈ (1..^𝑛)(𝑓𝑘))))) ≤ (𝑀𝐸))
12773, 126eqbrtrrd 5094 . . . 4 ((((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto𝐴) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
12858, 127exlimddv 1943 . . 3 (((𝜑 ∧ (𝑀𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
12943, 128pm2.61dane 3032 . 2 ((𝜑 ∧ (𝑀𝐸) ≠ +∞) → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
13015, 129pm2.61dane 3032 1 (𝜑 → ((𝑀‘(𝐸 𝐴)) +𝑒 (𝑀‘(𝐸 𝐴))) ≤ (𝑀𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wex 1787  wcel 2112  {cab 2716  wne 2943  wral 3064  wrex 3065  Vcvv 3423  cdif 3880  cin 3882  wss 3883  c0 4254  𝒫 cpw 4530   cuni 4836   ciun 4921  Disj wdisj 5035   class class class wbr 5070  cmpt 5152  ran crn 5570   Fn wfn 6396  wf 6397  ontowfo 6399  cfv 6401  (class class class)co 7235  ωcom 7666  cen 8647  cdom 8648  csdm 8649  Fincfn 8650  0cc0 10759  1c1 10760  +∞cpnf 10894  *cxr 10896   < clt 10897  cle 10898  cn 11860   +𝑒 cxad 12732  [,]cicc 12968  ..^cfzo 13268  Σ*cesum 31739  toCaraSigaccarsg 32012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-inf2 9286  ax-ac2 10107  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836  ax-pre-sup 10837  ax-addf 10838  ax-mulf 10839
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-disj 5036  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-se 5528  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-isom 6410  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-of 7491  df-om 7667  df-1st 7783  df-2nd 7784  df-supp 7928  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-1o 8226  df-2o 8227  df-er 8415  df-map 8534  df-pm 8535  df-ixp 8603  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-fsupp 9016  df-fi 9057  df-sup 9088  df-inf 9089  df-oi 9156  df-dju 9547  df-card 9585  df-acn 9588  df-ac 9760  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-div 11520  df-nn 11861  df-2 11923  df-3 11924  df-4 11925  df-5 11926  df-6 11927  df-7 11928  df-8 11929  df-9 11930  df-n0 12121  df-z 12207  df-dec 12324  df-uz 12469  df-q 12575  df-rp 12617  df-xneg 12734  df-xadd 12735  df-xmul 12736  df-ioo 12969  df-ioc 12970  df-ico 12971  df-icc 12972  df-fz 13126  df-fzo 13269  df-fl 13397  df-mod 13475  df-seq 13607  df-exp 13668  df-fac 13873  df-bc 13902  df-hash 13930  df-shft 14663  df-cj 14695  df-re 14696  df-im 14697  df-sqrt 14831  df-abs 14832  df-limsup 15065  df-clim 15082  df-rlim 15083  df-sum 15283  df-ef 15662  df-sin 15664  df-cos 15665  df-pi 15667  df-struct 16733  df-sets 16750  df-slot 16768  df-ndx 16778  df-base 16794  df-ress 16818  df-plusg 16848  df-mulr 16849  df-starv 16850  df-sca 16851  df-vsca 16852  df-ip 16853  df-tset 16854  df-ple 16855  df-ds 16857  df-unif 16858  df-hom 16859  df-cco 16860  df-rest 16960  df-topn 16961  df-0g 16979  df-gsum 16980  df-topgen 16981  df-pt 16982  df-prds 16985  df-ordt 17039  df-xrs 17040  df-qtop 17045  df-imas 17046  df-xps 17048  df-mre 17122  df-mrc 17123  df-acs 17125  df-ps 18105  df-tsr 18106  df-plusf 18146  df-mgm 18147  df-sgrp 18196  df-mnd 18207  df-mhm 18251  df-submnd 18252  df-grp 18401  df-minusg 18402  df-sbg 18403  df-mulg 18522  df-subg 18573  df-cntz 18744  df-cmn 19205  df-abl 19206  df-mgp 19538  df-ur 19550  df-ring 19597  df-cring 19598  df-subrg 19831  df-abv 19886  df-lmod 19934  df-scaf 19935  df-sra 20242  df-rgmod 20243  df-psmet 20388  df-xmet 20389  df-met 20390  df-bl 20391  df-mopn 20392  df-fbas 20393  df-fg 20394  df-cnfld 20397  df-top 21823  df-topon 21840  df-topsp 21862  df-bases 21875  df-cld 21948  df-ntr 21949  df-cls 21950  df-nei 22027  df-lp 22065  df-perf 22066  df-cn 22156  df-cnp 22157  df-haus 22244  df-tx 22491  df-hmeo 22684  df-fil 22775  df-fm 22867  df-flim 22868  df-flf 22869  df-tmd 23001  df-tgp 23002  df-tsms 23056  df-trg 23089  df-xms 23250  df-ms 23251  df-tms 23252  df-nm 23512  df-ngp 23513  df-nrg 23515  df-nlm 23516  df-ii 23806  df-cncf 23807  df-limc 24795  df-dv 24796  df-log 25477  df-esum 31740  df-carsg 32013
This theorem is referenced by:  carsgclctun  32032
  Copyright terms: Public domain W3C validator