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 47102

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 23	. . 3 ⊢ (𝜑 → 𝜑)
2		iftrue 4489	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
3	2	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
4		isomenndlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)
5		f1of 6810	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵⟶𝑌)
6	4, 5	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑌)
7		ssun1 4133	. . . . . . . . . . 11 ⊢ 𝑌 ⊆ (𝑌 ∪ {∅})
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ (𝑌 ∪ {∅}))
9	6, 8	fssd 6713	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐵⟶(𝑌 ∪ {∅}))
10	9	ffvelcdmda 7069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) ∈ (𝑌 ∪ {∅}))
11	3, 10	eqeltrd 2865	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
12	11	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13		iffalse 4492	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
14	13	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
15		0ex 5262	. . . . . . . . . . 11 ⊢ ∅ ∈ V
16	15	snid 4624	. . . . . . . . . 10 ⊢ ∅ ∈ {∅}
17		elun2 4138	. . . . . . . . . 10 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ∅ ∈ (𝑌 ∪ {∅})
19	18	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
20	14, 19	eqeltrd 2865	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
21	20	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
22	12, 21	pm2.61dan 824	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23		isomenndlem.a	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
24	22, 23	fmptd 7099	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
25		isomenndlem.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)
26		0elpw 5317	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑋
27		snssi 4747	. . . . . . 7 ⊢ (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
28	26, 27	ax-mp 5	. . . . . 6 ⊢ {∅} ⊆ 𝒫 𝑋
29	28	a1i 11	. . . . 5 ⊢ (𝜑 → {∅} ⊆ 𝒫 𝑋)
30	25, 29	unssd 4147	. . . 4 ⊢ (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
31	24, 30	fssd 6713	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 𝑋)
32		nnex 12230	. . . . . 6 ⊢ ℕ ∈ V
33	32	mptex 7211	. . . . 5 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ∈ V
34	23, 33	eqeltri 2861	. . . 4 ⊢ 𝐴 ∈ V
35		feq1 6673	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋 ↔ 𝐴:ℕ⟶𝒫 𝑋))
36	35	anbi2d 641	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋)))
37		fveq1 6870	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑎‘𝑛) = (𝐴‘𝑛))
38	37	iuneq2d 4983	. . . . . . 7 ⊢ (𝑎 = 𝐴 → ∪ 𝑛 ∈ ℕ (𝑎‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
39	38	fveq2d 6875	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
40		simpl 487	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → 𝑎 = 𝐴)
41	40	fveq1d 6873	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑎‘𝑛) = (𝐴‘𝑛))
42	41	fveq2d 6875	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝑎‘𝑛)) = (𝑂‘(𝐴‘𝑛)))
43	42	mpteq2dva 5198	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))
44	43	fveq2d 6875	. . . . . 6 ⊢ (𝑎 = 𝐴 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
45	39, 44	breq12d 5118	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
46	36, 45	imbi12d 347	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ↔ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))))
47		isomenndlem.subadd	. . . 4 ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))
48	34, 46, 47	vtocl 3528	. . 3 ⊢ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
49	1, 31, 48	syl2anc 595	. 2 ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
50	6	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵⟶𝑌)
51		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = ℕ → 𝐵 = ℕ)
53	52	eqcomd 2771	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ℕ → ℕ = 𝐵)
54	53	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
55	51, 54	eleqtrd 2867	. . . . . . . . . . . 12 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
56	55	adantll 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
57	50, 56	ffvelcdmd 7070	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑌)
58		eqid 2765	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))
59	57, 58	fmptd 7099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)
60	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)))
61	55	iftrued 4491	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
62	61	mpteq2dva 5198	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
63	60, 62	eqtrd 2800	. . . . . . . . . . 11 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
64	63	feq1d 6677	. . . . . . . . . 10 ⊢ (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
65	64	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
66	59, 65	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67		f1ofo 6818	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵–onto→𝑌)
68	4, 67	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐵–onto→𝑌)
69		dffo3 7087	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–onto→𝑌 ↔ (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
70	68, 69	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
71	70	simprd 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
72	71	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
73		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
74		rspa 3254	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
75	72, 73, 74	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
76	75	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
77		nfv 1937	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ 𝐵 = ℕ)
78		nfre1 3290	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)
79		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵)
80		simpl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝐵 = ℕ)
81	79, 80	eleqtrd 2867	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
82	81	adantll 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
83	82	3adant3 1148	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑛 ∈ ℕ)
84	60	fveq1d 6873	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = ℕ → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
85	84	3ad2ant1 1149	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
86		fvex 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
87	86, 15	ifex 4534	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
89		eqid 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
90	89	fvmpt2 6991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
91	81, 88, 90	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
92	2	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
93	91, 92	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
94	93	3adant3 1148	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
95		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝐹‘𝑛) → 𝑦 = (𝐹‘𝑛))
96	95	eqcomd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐹‘𝑛) → (𝐹‘𝑛) = 𝑦)
97	96	3ad2ant3 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐹‘𝑛) = 𝑦)
98	85, 94, 97	3eqtrrd 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
99	98	3adant1l 1193	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
100		rspe 3255	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
101	83, 99, 100	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
102	101	3exp 1135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ 𝐵 → (𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
103	77, 78, 102	rexlimd 3272	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
104	103	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
105	76, 104	mpd 16	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
106	105	ralrimiva 3157	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
107	66, 106	jca 520	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
108		dffo3 7087	. . . . . . 7 ⊢ (𝐴:ℕ–onto→𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
109	107, 108	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ–onto→𝑌)
110		founiiun 45755	. . . . . 6 ⊢ (𝐴:ℕ–onto→𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
111	109, 110	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
112		uniun 4891	. . . . . . . 8 ⊢ ∪ (𝑌 ∪ {∅}) = (∪ 𝑌 ∪ ∪ {∅})
113	15	unisn 4887	. . . . . . . . 9 ⊢ ∪ {∅} = ∅
114	113	uneq2i 4121	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∪ {∅}) = (∪ 𝑌 ∪ ∅)
115		un0 4351	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∅) = ∪ 𝑌
116	112, 114, 115	3eqtrri 2793	. . . . . . 7 ⊢ ∪ 𝑌 = ∪ (𝑌 ∪ {∅})
117	116	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ (𝑌 ∪ {∅}))
118	24	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119		nfv 1937	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120		isomenndlem.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℕ)
121	120	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
122	52	necon3bi 2986	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝐵 = ℕ → 𝐵 ≠ ℕ)
123	122	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124	121, 123	jca 520	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125		df-pss 3927	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126	124, 125	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127		pssnel 4428	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
128	126, 127	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
129	128	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
130		simprl 782	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
131		simprl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
132	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
133	23	fvmpt2 6991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
134	131, 132, 133	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
135	134	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
136	13	ad2antll 741	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
137		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
138	137	eqcomd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
139	138	ad2antlr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∅ = 𝑦)
140	135, 136, 139	3eqtrrd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑦 = (𝐴‘𝑛))
141	130, 140, 100	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
142	141	ex 417	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
143	142	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
144	119, 78, 129, 143	exlimimdd 2257	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
145	144	adantlr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
146		simplll 786	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148		elsni 4602	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
149	148	con3i 155	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150	149	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151		elunnel2 4111	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦 ∈ 𝑌)
152	147, 150, 151	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
153	152	adantll 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
154	68	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐵–onto→𝑌)
155		foelcdmi 6932	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–onto→𝑌 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
156	154, 73, 155	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
157		nfv 1937	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑦 ∈ 𝑌)
158	120	sselda 3939	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
159	158	3adant3 1148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160	158, 87, 133	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
161	160, 3	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = (𝐹‘𝑛))
162	161	3adant3 1148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐴‘𝑛) = (𝐹‘𝑛))
163		simp3 1154	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐹‘𝑛) = 𝑦)
164	162, 163	eqtr2d 2801	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑦 = (𝐴‘𝑛))
165	159, 164, 100	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
166	165	3exp 1135	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
167	166	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
168	157, 78, 167	rexlimd 3272	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
169	156, 168	mpd 16	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
170	146, 153, 169	syl2anc 595	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
171	145, 170	pm2.61dan 824	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
172	171	ralrimiva 3157	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
173	118, 172	jca 520	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
174		dffo3 7087	. . . . . . . 8 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
175	173, 174	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176		founiiun 45755	. . . . . . 7 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
177	175, 176	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
178	117, 177	eqtrd 2800	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
179	111, 178	pm2.61dan 824	. . . 4 ⊢ (𝜑 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
180	179	fveq2d 6875	. . 3 ⊢ (𝜑 → (𝑂‘∪ 𝑌) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
181		uncom 4114	. . . . . . . . 9 ⊢ ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182	181	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183		undif 4439	. . . . . . . . 9 ⊢ (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184	120, 183	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185	182, 184	eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186	185	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187	186	mpteq1d 5195	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))))
188	187	fveq2d 6875	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))))
189		nfv 1937	. . . . 5 ⊢ Ⅎ𝑛𝜑
190		difexg 5290	. . . . . . 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 5285	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
195		disjdifr 4430	. . . . . 6 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
196	195	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
197		simpl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
198		eldifi 4087	. . . . . . 7 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
199	198	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
200		isomenndlem.o	. . . . . . . 8 ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
201	200	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
202	31	ffvelcdmda 7069	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
203	201, 202	ffvelcdmd 7070	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
204	197, 199, 203	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
205	158, 203	syldan 602	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
206	189, 192, 194, 196, 204, 205	sge0splitmpt 46983	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
207		eqid 2765	. . . . . . . 8 ⊢ (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))
208	205, 207	fmptd 7099	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))):𝐵⟶(0[,]+∞))
209	194, 208	sge0xrcl 46957	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) ∈ ℝ^*)
210	209	xaddlidd 45895	. . . . 5 ⊢ (𝜑 → (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
211	87	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
212	199, 211, 133	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
213		eldifn 4088	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛 ∈ 𝐵)
214	213	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛 ∈ 𝐵)
215	214	iffalsed 4494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
216	212, 215	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = ∅)
217	216	fveq2d 6875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = (𝑂‘∅))
218		isomenndlem.o0	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∅) = 0)
219	197, 218	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
220	217, 219	eqtrd 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = 0)
221	220	mpteq2dva 5198	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
222	221	fveq2d 6875	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
223	189, 192	sge0z 46947	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
224	222, 223	eqtrd 2800	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = 0)
225	224	oveq1d 7415	. . . . 5 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
226	200, 25	feqresmpt 6940	. . . . . . 7 ⊢ (𝜑 → (𝑂 ↾ 𝑌) = (𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦)))
227	226	fveq2d 6875	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))))
228		nfv 1937	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
229		fveq2 6871	. . . . . . 7 ⊢ (𝑦 = (𝐴‘𝑛) → (𝑂‘𝑦) = (𝑂‘(𝐴‘𝑛)))
230	161	eqcomd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = (𝐴‘𝑛))
231	200	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
232	25	sselda 3939	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝒫 𝑋)
233	231, 232	ffvelcdmd 7070	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑂‘𝑦) ∈ (0[,]+∞))
234	228, 189, 229, 194, 4, 230, 233	sge0f1o 46954	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
235		eqidd 2766	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
236	227, 234, 235	3eqtrd 2804	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
237	210, 225, 236	3eqtr4d 2810	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑂 ↾ 𝑌)))
238	188, 206, 237	3eqtrrd 2805	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
239	180, 238	breq12d 5118	. 2 ⊢ (𝜑 → ((𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
240	49, 239	mpbird 260	1 ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∃wex 1802 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 ∃wrex 3089 Vcvv 3457 ∖ cdif 3904 ∪ cun 3905 ∩ cin 3906 ⊆ wss 3907 ⊊ wpss 3908 ∅c0 4288 ifcif 4483 𝒫 cpw 4558 {csn 4585 ∪ cuni 4868 ∪ ciun 4952 class class class wbr 5105 ↦ cmpt 5186 ↾ cres 5654 ⟶wf 6521 –onto→wfo 6523 –1-1-onto→wf1o 6524 ‘cfv 6525 (class class class)co 7400 0cc0 11088 +∞cpnf 11228 ≤ cle 11232 ℕcn 12224 +_𝑒 cxad 13126 [,]cicc 13366 Σ^{^}csumge0 46934

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-sup 9390 df-oi 9460 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-n0 12496 df-z 12583 df-uz 12854 df-rp 13008 df-xadd 13129 df-ico 13369 df-icc 13370 df-fz 13527 df-fzo 13674 df-seq 14029 df-exp 14089 df-hash 14358 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-clim 15529 df-sum 15728 df-sumge0 46935

This theorem is referenced by: isomennd 47103

W3C validator