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 46882

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 4487	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
3	2	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
4		isomenndlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)
5		f1of 6782	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵⟶𝑌)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑌)
7		ssun1 4132	. . . . . . . . . . 11 ⊢ 𝑌 ⊆ (𝑌 ∪ {∅})
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ (𝑌 ∪ {∅}))
9	6, 8	fssd 6687	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐵⟶(𝑌 ∪ {∅}))
10	9	ffvelcdmda 7038	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) ∈ (𝑌 ∪ {∅}))
11	3, 10	eqeltrd 2837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
12	11	adantlr 716	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13		iffalse 4490	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
14	13	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
15		0ex 5254	. . . . . . . . . . 11 ⊢ ∅ ∈ V
16	15	snid 4621	. . . . . . . . . 10 ⊢ ∅ ∈ {∅}
17		elun2 4137	. . . . . . . . . 10 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ∅ ∈ (𝑌 ∪ {∅})
19	18	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
20	14, 19	eqeltrd 2837	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
21	20	adantlr 716	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
22	12, 21	pm2.61dan 813	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23		isomenndlem.a	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
24	22, 23	fmptd 7068	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
25		isomenndlem.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)
26		0elpw 5303	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑋
27		snssi 4766	. . . . . . 7 ⊢ (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
28	26, 27	ax-mp 5	. . . . . 6 ⊢ {∅} ⊆ 𝒫 𝑋
29	28	a1i 11	. . . . 5 ⊢ (𝜑 → {∅} ⊆ 𝒫 𝑋)
30	25, 29	unssd 4146	. . . 4 ⊢ (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
31	24, 30	fssd 6687	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 𝑋)
32		nnex 12163	. . . . . 6 ⊢ ℕ ∈ V
33	32	mptex 7179	. . . . 5 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ∈ V
34	23, 33	eqeltri 2833	. . . 4 ⊢ 𝐴 ∈ V
35		feq1 6648	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋 ↔ 𝐴:ℕ⟶𝒫 𝑋))
36	35	anbi2d 631	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋)))
37		fveq1 6841	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑎‘𝑛) = (𝐴‘𝑛))
38	37	iuneq2d 4979	. . . . . . 7 ⊢ (𝑎 = 𝐴 → ∪ 𝑛 ∈ ℕ (𝑎‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
39	38	fveq2d 6846	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
40		simpl 482	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → 𝑎 = 𝐴)
41	40	fveq1d 6844	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑎‘𝑛) = (𝐴‘𝑛))
42	41	fveq2d 6846	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝑎‘𝑛)) = (𝑂‘(𝐴‘𝑛)))
43	42	mpteq2dva 5193	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))
44	43	fveq2d 6846	. . . . . 6 ⊢ (𝑎 = 𝐴 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
45	39, 44	breq12d 5113	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
46	36, 45	imbi12d 344	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ↔ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))))
47		isomenndlem.subadd	. . . 4 ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))
48	34, 46, 47	vtocl 3517	. . 3 ⊢ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
49	1, 31, 48	syl2anc 585	. 2 ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
50	6	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵⟶𝑌)
51		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = ℕ → 𝐵 = ℕ)
53	52	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ℕ → ℕ = 𝐵)
54	53	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
55	51, 54	eleqtrd 2839	. . . . . . . . . . . 12 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
56	55	adantll 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
57	50, 56	ffvelcdmd 7039	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑌)
58		eqid 2737	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))
59	57, 58	fmptd 7068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)
60	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)))
61	55	iftrued 4489	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
62	61	mpteq2dva 5193	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
63	60, 62	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
64	63	feq1d 6652	. . . . . . . . . 10 ⊢ (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
65	64	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
66	59, 65	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67		f1ofo 6789	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵–onto→𝑌)
68	4, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐵–onto→𝑌)
69		dffo3 7056	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–onto→𝑌 ↔ (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
70	68, 69	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
71	70	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
72	71	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
73		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
74		rspa 3227	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
75	72, 73, 74	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
76	75	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
77		nfv 1916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ 𝐵 = ℕ)
78		nfre1 3263	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)
79		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵)
80		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝐵 = ℕ)
81	79, 80	eleqtrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
82	81	adantll 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
83	82	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑛 ∈ ℕ)
84	60	fveq1d 6844	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = ℕ → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
85	84	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
86		fvex 6855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
87	86, 15	ifex 4532	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
89		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
90	89	fvmpt2 6961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
91	81, 88, 90	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
92	2	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
93	91, 92	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
94	93	3adant3 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
95		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝐹‘𝑛) → 𝑦 = (𝐹‘𝑛))
96	95	eqcomd 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐹‘𝑛) → (𝐹‘𝑛) = 𝑦)
97	96	3ad2ant3 1136	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐹‘𝑛) = 𝑦)
98	85, 94, 97	3eqtrrd 2777	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
99	98	3adant1l 1178	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
100		rspe 3228	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
101	83, 99, 100	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
102	101	3exp 1120	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ 𝐵 → (𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
103	77, 78, 102	rexlimd 3245	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
104	103	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
105	76, 104	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
106	105	ralrimiva 3130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
107	66, 106	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
108		dffo3 7056	. . . . . . 7 ⊢ (𝐴:ℕ–onto→𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
109	107, 108	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ–onto→𝑌)
110		founiiun 45532	. . . . . 6 ⊢ (𝐴:ℕ–onto→𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
111	109, 110	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
112		uniun 4888	. . . . . . . 8 ⊢ ∪ (𝑌 ∪ {∅}) = (∪ 𝑌 ∪ ∪ {∅})
113	15	unisn 4884	. . . . . . . . 9 ⊢ ∪ {∅} = ∅
114	113	uneq2i 4119	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∪ {∅}) = (∪ 𝑌 ∪ ∅)
115		un0 4348	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∅) = ∪ 𝑌
116	112, 114, 115	3eqtrri 2765	. . . . . . 7 ⊢ ∪ 𝑌 = ∪ (𝑌 ∪ {∅})
117	116	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ (𝑌 ∪ {∅}))
118	24	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120		isomenndlem.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℕ)
121	120	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
122	52	necon3bi 2959	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝐵 = ℕ → 𝐵 ≠ ℕ)
123	122	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124	121, 123	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125		df-pss 3923	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126	124, 125	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127		pssnel 4425	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
128	126, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
129	128	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
130		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
131		simprl 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
132	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
133	23	fvmpt2 6961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
134	131, 132, 133	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
135	134	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
136	13	ad2antll 730	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
137		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
138	137	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
139	138	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∅ = 𝑦)
140	135, 136, 139	3eqtrrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑦 = (𝐴‘𝑛))
141	130, 140, 100	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
142	141	ex 412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
143	142	adantlr 716	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
144	119, 78, 129, 143	exlimimdd 2227	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
145	144	adantlr 716	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
146		simplll 775	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148		elsni 4599	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
149	148	con3i 154	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150	149	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151		elunnel2 4109	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦 ∈ 𝑌)
152	147, 150, 151	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
153	152	adantll 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
154	68	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐵–onto→𝑌)
155		foelcdmi 6903	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–onto→𝑌 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
156	154, 73, 155	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
157		nfv 1916	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑦 ∈ 𝑌)
158	120	sselda 3935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
159	158	3adant3 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160	158, 87, 133	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
161	160, 3	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = (𝐹‘𝑛))
162	161	3adant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐴‘𝑛) = (𝐹‘𝑛))
163		simp3 1139	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐹‘𝑛) = 𝑦)
164	162, 163	eqtr2d 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑦 = (𝐴‘𝑛))
165	159, 164, 100	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
166	165	3exp 1120	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
167	166	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
168	157, 78, 167	rexlimd 3245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
169	156, 168	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
170	146, 153, 169	syl2anc 585	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
171	145, 170	pm2.61dan 813	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
172	171	ralrimiva 3130	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
173	118, 172	jca 511	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
174		dffo3 7056	. . . . . . . 8 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
175	173, 174	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176		founiiun 45532	. . . . . . 7 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
177	175, 176	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
178	117, 177	eqtrd 2772	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
179	111, 178	pm2.61dan 813	. . . 4 ⊢ (𝜑 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
180	179	fveq2d 6846	. . 3 ⊢ (𝜑 → (𝑂‘∪ 𝑌) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
181		uncom 4112	. . . . . . . . 9 ⊢ ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182	181	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183		undif 4436	. . . . . . . . 9 ⊢ (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184	120, 183	sylib 218	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185	182, 184	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186	185	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187	186	mpteq1d 5190	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))))
188	187	fveq2d 6846	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))))
189		nfv 1916	. . . . 5 ⊢ Ⅎ𝑛𝜑
190		difexg 5276	. . . . . . 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 5271	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
195		disjdifr 4427	. . . . . 6 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
196	195	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
197		simpl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
198		eldifi 4085	. . . . . . 7 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
199	198	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
200		isomenndlem.o	. . . . . . . 8 ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
201	200	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
202	31	ffvelcdmda 7038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
203	201, 202	ffvelcdmd 7039	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
204	197, 199, 203	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
205	158, 203	syldan 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
206	189, 192, 194, 196, 204, 205	sge0splitmpt 46763	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
207		eqid 2737	. . . . . . . 8 ⊢ (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))
208	205, 207	fmptd 7068	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))):𝐵⟶(0[,]+∞))
209	194, 208	sge0xrcl 46737	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) ∈ ℝ^*)
210	209	xaddlidd 45674	. . . . 5 ⊢ (𝜑 → (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
211	87	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
212	199, 211, 133	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
213		eldifn 4086	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛 ∈ 𝐵)
214	213	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛 ∈ 𝐵)
215	214	iffalsed 4492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
216	212, 215	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = ∅)
217	216	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = (𝑂‘∅))
218		isomenndlem.o0	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∅) = 0)
219	197, 218	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
220	217, 219	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = 0)
221	220	mpteq2dva 5193	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
222	221	fveq2d 6846	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
223	189, 192	sge0z 46727	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
224	222, 223	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = 0)
225	224	oveq1d 7383	. . . . 5 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
226	200, 25	feqresmpt 6911	. . . . . . 7 ⊢ (𝜑 → (𝑂 ↾ 𝑌) = (𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦)))
227	226	fveq2d 6846	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))))
228		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
229		fveq2 6842	. . . . . . 7 ⊢ (𝑦 = (𝐴‘𝑛) → (𝑂‘𝑦) = (𝑂‘(𝐴‘𝑛)))
230	161	eqcomd 2743	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = (𝐴‘𝑛))
231	200	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
232	25	sselda 3935	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝒫 𝑋)
233	231, 232	ffvelcdmd 7039	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑂‘𝑦) ∈ (0[,]+∞))
234	228, 189, 229, 194, 4, 230, 233	sge0f1o 46734	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
235		eqidd 2738	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
236	227, 234, 235	3eqtrd 2776	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
237	210, 225, 236	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑂 ↾ 𝑌)))
238	188, 206, 237	3eqtrrd 2777	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
239	180, 238	breq12d 5113	. 2 ⊢ (𝜑 → ((𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
240	49, 239	mpbird 257	1 ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ⊊ wpss 3904 ∅c0 4287 ifcif 4481 𝒫 cpw 4556 {csn 4582 ∪ cuni 4865 ∪ ciun 4948 class class class wbr 5100 ↦ cmpt 5181 ↾ cres 5634 ⟶wf 6496 –onto→wfo 6498 –1-1-onto→wf1o 6499 ‘cfv 6500 (class class class)co 7368 0cc0 11038 +∞cpnf 11175 ≤ cle 11179 ℕcn 12157 +_𝑒 cxad 13036 [,]cicc 13276 Σ^{^}csumge0 46714

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-z 12501 df-uz 12764 df-rp 12918 df-xadd 13039 df-ico 13279 df-icc 13280 df-fz 13436 df-fzo 13583 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-clim 15423 df-sum 15622 df-sumge0 46715

This theorem is referenced by: isomennd 46883

W3C validator