isomenndlem - Mathbox for Glauco Siliprandi

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

Theorem isomenndlem 42243

Description: 𝑂 is sub-additive w.r.t. countable indexed union, implies that 𝑂 is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypotheses**
Ref	Expression
isomenndlem.o	⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
isomenndlem.o0	⊢ (𝜑 → (𝑂‘∅) = 0)
isomenndlem.y	⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)
isomenndlem.subadd	⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))
isomenndlem.b	⊢ (𝜑 → 𝐵 ⊆ ℕ)
isomenndlem.f	⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)
isomenndlem.a	⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))

**Assertion**
Ref	Expression
isomenndlem	⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)))

Distinct variable groups: 𝐴,𝑎,𝑛 𝐵,𝑛 𝑛,𝐹 𝑂,𝑎,𝑛 𝑋,𝑎 𝑛,𝑌 𝜑,𝑎,𝑛 Allowed substitution hints: 𝐵(𝑎) 𝐹(𝑎) 𝑋(𝑛) 𝑌(𝑎)

Proof of Theorem isomenndlem Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝜑 → 𝜑)
2		iftrue 4350	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
3	2	adantl 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
4		isomenndlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)
5		f1of 6438	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵⟶𝑌)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑌)
7		ssun1 4031	. . . . . . . . . . 11 ⊢ 𝑌 ⊆ (𝑌 ∪ {∅})
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ (𝑌 ∪ {∅}))
9	6, 8	fssd 6352	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐵⟶(𝑌 ∪ {∅}))
10	9	ffvelrnda 6670	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) ∈ (𝑌 ∪ {∅}))
11	3, 10	eqeltrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
12	11	adantlr 702	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13		iffalse 4353	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
14	13	adantl 474	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
15		0ex 5062	. . . . . . . . . . 11 ⊢ ∅ ∈ V
16	15	snid 4467	. . . . . . . . . 10 ⊢ ∅ ∈ {∅}
17		elun2 4036	. . . . . . . . . 10 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ∅ ∈ (𝑌 ∪ {∅})
19	18	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
20	14, 19	eqeltrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
21	20	adantlr 702	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
22	12, 21	pm2.61dan 800	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23		isomenndlem.a	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
24	22, 23	fmptd 6695	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
25		isomenndlem.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)
26		0elpw 5104	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑋
27		snssi 4609	. . . . . . 7 ⊢ (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
28	26, 27	ax-mp 5	. . . . . 6 ⊢ {∅} ⊆ 𝒫 𝑋
29	28	a1i 11	. . . . 5 ⊢ (𝜑 → {∅} ⊆ 𝒫 𝑋)
30	25, 29	unssd 4044	. . . 4 ⊢ (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
31	24, 30	fssd 6352	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 𝑋)
32		nnex 11440	. . . . . 6 ⊢ ℕ ∈ V
33	32	mptex 6806	. . . . 5 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ∈ V
34	23, 33	eqeltri 2856	. . . 4 ⊢ 𝐴 ∈ V
35		feq1 6319	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋 ↔ 𝐴:ℕ⟶𝒫 𝑋))
36	35	anbi2d 619	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋)))
37		fveq1 6492	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑎‘𝑛) = (𝐴‘𝑛))
38	37	iuneq2d 4814	. . . . . . 7 ⊢ (𝑎 = 𝐴 → ∪ 𝑛 ∈ ℕ (𝑎‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
39	38	fveq2d 6497	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
40		simpl 475	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → 𝑎 = 𝐴)
41	40	fveq1d 6495	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑎‘𝑛) = (𝐴‘𝑛))
42	41	fveq2d 6497	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝑎‘𝑛)) = (𝑂‘(𝐴‘𝑛)))
43	42	mpteq2dva 5016	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))
44	43	fveq2d 6497	. . . . . 6 ⊢ (𝑎 = 𝐴 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
45	39, 44	breq12d 4936	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
46	36, 45	imbi12d 337	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ↔ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))))
47		isomenndlem.subadd	. . . 4 ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))
48	34, 46, 47	vtocl 3472	. . 3 ⊢ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
49	1, 31, 48	syl2anc 576	. 2 ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
50	6	ad2antrr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵⟶𝑌)
51		simpr 477	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = ℕ → 𝐵 = ℕ)
53	52	eqcomd 2778	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ℕ → ℕ = 𝐵)
54	53	adantr 473	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
55	51, 54	eleqtrd 2862	. . . . . . . . . . . 12 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
56	55	adantll 701	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
57	50, 56	ffvelrnd 6671	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑌)
58		eqid 2772	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))
59	57, 58	fmptd 6695	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)
60	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)))
61	55	iftrued 4352	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
62	61	mpteq2dva 5016	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
63	60, 62	eqtrd 2808	. . . . . . . . . . 11 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
64	63	feq1d 6323	. . . . . . . . . 10 ⊢ (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
65	64	adantl 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
66	59, 65	mpbird 249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67		f1ofo 6445	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵–onto→𝑌)
68	4, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐵–onto→𝑌)
69		dffo3 6685	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–onto→𝑌 ↔ (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
70	68, 69	sylib 210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
71	70	simprd 488	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
72	71	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
73		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
74		rspa 3150	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
75	72, 73, 74	syl2anc 576	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
76	75	adantlr 702	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
77		nfv 1873	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ 𝐵 = ℕ)
78		nfre1 3245	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)
79		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵)
80		simpl 475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝐵 = ℕ)
81	79, 80	eleqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
82	81	adantll 701	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
83	82	3adant3 1112	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑛 ∈ ℕ)
84	60	fveq1d 6495	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = ℕ → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
85	84	3ad2ant1 1113	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
86		fvex 6506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
87	86, 15	ifex 4392	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
89		eqid 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
90	89	fvmpt2 6599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
91	81, 88, 90	syl2anc 576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
92	2	adantl 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
93	91, 92	eqtrd 2808	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
94	93	3adant3 1112	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
95		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝐹‘𝑛) → 𝑦 = (𝐹‘𝑛))
96	95	eqcomd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐹‘𝑛) → (𝐹‘𝑛) = 𝑦)
97	96	3ad2ant3 1115	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐹‘𝑛) = 𝑦)
98	85, 94, 97	3eqtrrd 2813	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
99	98	3adant1l 1156	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
100		rspe 3243	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
101	83, 99, 100	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
102	101	3exp 1099	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ 𝐵 → (𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
103	77, 78, 102	rexlimd 3254	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
104	103	adantr 473	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
105	76, 104	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
106	105	ralrimiva 3126	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
107	66, 106	jca 504	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
108		dffo3 6685	. . . . . . 7 ⊢ (𝐴:ℕ–onto→𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
109	107, 108	sylibr 226	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ–onto→𝑌)
110		founiiun 40859	. . . . . 6 ⊢ (𝐴:ℕ–onto→𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
111	109, 110	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
112		uniun 4725	. . . . . . . 8 ⊢ ∪ (𝑌 ∪ {∅}) = (∪ 𝑌 ∪ ∪ {∅})
113	15	unisn 4722	. . . . . . . . 9 ⊢ ∪ {∅} = ∅
114	113	uneq2i 4019	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∪ {∅}) = (∪ 𝑌 ∪ ∅)
115		un0 4224	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∅) = ∪ 𝑌
116	112, 114, 115	3eqtrri 2801	. . . . . . 7 ⊢ ∪ 𝑌 = ∪ (𝑌 ∪ {∅})
117	116	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ (𝑌 ∪ {∅}))
118	24	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119		nfv 1873	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120		isomenndlem.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℕ)
121	120	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
122	52	necon3bi 2987	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝐵 = ℕ → 𝐵 ≠ ℕ)
123	122	adantl 474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124	121, 123	jca 504	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125		df-pss 3839	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126	124, 125	sylibr 226	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127		pssnel 4297	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
128	126, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
129	128	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
130		simprl 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
131		simprl 758	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
132	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
133	23	fvmpt2 6599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
134	131, 132, 133	syl2anc 576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
135	134	adantlr 702	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
136	13	ad2antll 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
137		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
138	137	eqcomd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
139	138	ad2antlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∅ = 𝑦)
140	135, 136, 139	3eqtrrd 2813	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑦 = (𝐴‘𝑛))
141	130, 140, 100	syl2anc 576	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
142	141	ex 405	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
143	142	adantlr 702	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
144	119, 78, 129, 143	exlimimdd 2149	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
145	144	adantlr 702	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
146		simplll 762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147		simpl 475	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148		elsni 4452	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
149	148	con3i 152	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150	149	adantl 474	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151		elunnel2 40715	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦 ∈ 𝑌)
152	147, 150, 151	syl2anc 576	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
153	152	adantll 701	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
154	68	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐵–onto→𝑌)
155		foelrni 6551	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–onto→𝑌 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
156	154, 73, 155	syl2anc 576	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
157		nfv 1873	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑦 ∈ 𝑌)
158	120	sselda 3852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
159	158	3adant3 1112	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160	158, 87, 133	sylancl 577	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
161	160, 3	eqtrd 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = (𝐹‘𝑛))
162	161	3adant3 1112	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐴‘𝑛) = (𝐹‘𝑛))
163		simp3 1118	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐹‘𝑛) = 𝑦)
164	162, 163	eqtr2d 2809	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑦 = (𝐴‘𝑛))
165	159, 164, 100	syl2anc 576	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
166	165	3exp 1099	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
167	166	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
168	157, 78, 167	rexlimd 3254	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
169	156, 168	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
170	146, 153, 169	syl2anc 576	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
171	145, 170	pm2.61dan 800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
172	171	ralrimiva 3126	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
173	118, 172	jca 504	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
174		dffo3 6685	. . . . . . . 8 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
175	173, 174	sylibr 226	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176		founiiun 40859	. . . . . . 7 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
177	175, 176	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
178	117, 177	eqtrd 2808	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
179	111, 178	pm2.61dan 800	. . . 4 ⊢ (𝜑 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
180	179	fveq2d 6497	. . 3 ⊢ (𝜑 → (𝑂‘∪ 𝑌) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
181		uncom 4012	. . . . . . . . 9 ⊢ ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182	181	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183		undif 4307	. . . . . . . . 9 ⊢ (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184	120, 183	sylib 210	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185	182, 184	eqtrd 2808	. . . . . . 7 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186	185	eqcomd 2778	. . . . . 6 ⊢ (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187	186	mpteq1d 5010	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))))
188	187	fveq2d 6497	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))))
189		nfv 1873	. . . . 5 ⊢ Ⅎ𝑛𝜑
190		difexg 5081	. . . . . . 7 ⊢ (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
191	32, 190	ax-mp 5	. . . . . 6 ⊢ (ℕ ∖ 𝐵) ∈ V
192	191	a1i 11	. . . . 5 ⊢ (𝜑 → (ℕ ∖ 𝐵) ∈ V)
193	32	a1i 11	. . . . . 6 ⊢ (𝜑 → ℕ ∈ V)
194	193, 120	ssexd 5078	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
195		incom 4060	. . . . . . 7 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (ℕ ∖ 𝐵))
196		disjdif 4298	. . . . . . 7 ⊢ (𝐵 ∩ (ℕ ∖ 𝐵)) = ∅
197	195, 196	eqtri 2796	. . . . . 6 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
198	197	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
199		simpl 475	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
200		eldifi 3987	. . . . . . 7 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
201	200	adantl 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
202		isomenndlem.o	. . . . . . . 8 ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
203	202	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
204	31	ffvelrnda 6670	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
205	203, 204	ffvelrnd 6671	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
206	199, 201, 205	syl2anc 576	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
207	158, 205	syldan 582	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
208	189, 192, 194, 198, 206, 207	sge0splitmpt 42124	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
209		eqid 2772	. . . . . . . 8 ⊢ (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))
210	207, 209	fmptd 6695	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))):𝐵⟶(0[,]+∞))
211	194, 210	sge0xrcl 42098	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) ∈ ℝ^*)
212	211	xaddid2d 41016	. . . . 5 ⊢ (𝜑 → (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
213	87	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
214	201, 213, 133	syl2anc 576	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
215		eldifn 3988	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛 ∈ 𝐵)
216	215	adantl 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛 ∈ 𝐵)
217	216	iffalsed 4355	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
218	214, 217	eqtrd 2808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = ∅)
219	218	fveq2d 6497	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = (𝑂‘∅))
220		isomenndlem.o0	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∅) = 0)
221	199, 220	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
222	219, 221	eqtrd 2808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = 0)
223	222	mpteq2dva 5016	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
224	223	fveq2d 6497	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
225	189, 192	sge0z 42088	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
226	224, 225	eqtrd 2808	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = 0)
227	226	oveq1d 6985	. . . . 5 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
228	202, 25	feqresmpt 6557	. . . . . . 7 ⊢ (𝜑 → (𝑂 ↾ 𝑌) = (𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦)))
229	228	fveq2d 6497	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))))
230		nfv 1873	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
231		fveq2 6493	. . . . . . 7 ⊢ (𝑦 = (𝐴‘𝑛) → (𝑂‘𝑦) = (𝑂‘(𝐴‘𝑛)))
232	161	eqcomd 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = (𝐴‘𝑛))
233	202	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
234	25	sselda 3852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝒫 𝑋)
235	233, 234	ffvelrnd 6671	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑂‘𝑦) ∈ (0[,]+∞))
236	230, 189, 231, 194, 4, 232, 235	sge0f1o 42095	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
237		eqidd 2773	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
238	229, 236, 237	3eqtrd 2812	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
239	212, 227, 238	3eqtr4d 2818	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑂 ↾ 𝑌)))
240	188, 208, 239	3eqtrrd 2813	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
241	180, 240	breq12d 4936	. 2 ⊢ (𝜑 → ((𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
242	49, 241	mpbird 249	1 ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∃wex 1742 ∈ wcel 2050 ≠ wne 2961 ∀wral 3082 ∃wrex 3083 Vcvv 3409 ∖ cdif 3820 ∪ cun 3821 ∩ cin 3822 ⊆ wss 3823 ⊊ wpss 3824 ∅c0 4172 ifcif 4344 𝒫 cpw 4416 {csn 4435 ∪ cuni 4706 ∪ ciun 4786 class class class wbr 4923 ↦ cmpt 5002 ↾ cres 5403 ⟶wf 6178 –onto→wfo 6180 –1-1-onto→wf1o 6181 ‘cfv 6182 (class class class)co 6970 0cc0 10329 +∞cpnf 10465 ≤ cle 10469 ℕcn 11433 +_𝑒 cxad 12316 [,]cicc 12551 Σ^{^}csumge0 42075

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-inf2 8892 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 ax-pre-sup 10407

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-se 5361 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-isom 6191 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7495 df-2nd 7496 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-1o 7899 df-oadd 7903 df-er 8083 df-en 8301 df-dom 8302 df-sdom 8303 df-fin 8304 df-sup 8695 df-oi 8763 df-card 9156 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-div 11093 df-nn 11434 df-2 11497 df-3 11498 df-n0 11702 df-z 11788 df-uz 12053 df-rp 12199 df-xadd 12319 df-ico 12554 df-icc 12555 df-fz 12703 df-fzo 12844 df-seq 13179 df-exp 13239 df-hash 13500 df-cj 14313 df-re 14314 df-im 14315 df-sqrt 14449 df-abs 14450 df-clim 14700 df-sum 14898 df-sumge0 42076

This theorem is referenced by: isomennd 42244

W3C validator