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 45246

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 4535	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
3	2	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
4		isomenndlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)
5		f1of 6834	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵⟶𝑌)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑌)
7		ssun1 4173	. . . . . . . . . . 11 ⊢ 𝑌 ⊆ (𝑌 ∪ {∅})
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ (𝑌 ∪ {∅}))
9	6, 8	fssd 6736	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐵⟶(𝑌 ∪ {∅}))
10	9	ffvelcdmda 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) ∈ (𝑌 ∪ {∅}))
11	3, 10	eqeltrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
12	11	adantlr 714	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13		iffalse 4538	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
14	13	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
15		0ex 5308	. . . . . . . . . . 11 ⊢ ∅ ∈ V
16	15	snid 4665	. . . . . . . . . 10 ⊢ ∅ ∈ {∅}
17		elun2 4178	. . . . . . . . . 10 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ∅ ∈ (𝑌 ∪ {∅})
19	18	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
20	14, 19	eqeltrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
21	20	adantlr 714	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
22	12, 21	pm2.61dan 812	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23		isomenndlem.a	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
24	22, 23	fmptd 7114	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
25		isomenndlem.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)
26		0elpw 5355	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑋
27		snssi 4812	. . . . . . 7 ⊢ (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
28	26, 27	ax-mp 5	. . . . . 6 ⊢ {∅} ⊆ 𝒫 𝑋
29	28	a1i 11	. . . . 5 ⊢ (𝜑 → {∅} ⊆ 𝒫 𝑋)
30	25, 29	unssd 4187	. . . 4 ⊢ (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
31	24, 30	fssd 6736	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 𝑋)
32		nnex 12218	. . . . . 6 ⊢ ℕ ∈ V
33	32	mptex 7225	. . . . 5 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ∈ V
34	23, 33	eqeltri 2830	. . . 4 ⊢ 𝐴 ∈ V
35		feq1 6699	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋 ↔ 𝐴:ℕ⟶𝒫 𝑋))
36	35	anbi2d 630	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋)))
37		fveq1 6891	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑎‘𝑛) = (𝐴‘𝑛))
38	37	iuneq2d 5027	. . . . . . 7 ⊢ (𝑎 = 𝐴 → ∪ 𝑛 ∈ ℕ (𝑎‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
39	38	fveq2d 6896	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
40		simpl 484	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → 𝑎 = 𝐴)
41	40	fveq1d 6894	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑎‘𝑛) = (𝐴‘𝑛))
42	41	fveq2d 6896	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝑎‘𝑛)) = (𝑂‘(𝐴‘𝑛)))
43	42	mpteq2dva 5249	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))
44	43	fveq2d 6896	. . . . . 6 ⊢ (𝑎 = 𝐴 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
45	39, 44	breq12d 5162	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
46	36, 45	imbi12d 345	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ↔ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))))
47		isomenndlem.subadd	. . . 4 ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))
48	34, 46, 47	vtocl 3550	. . 3 ⊢ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
49	1, 31, 48	syl2anc 585	. 2 ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
50	6	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵⟶𝑌)
51		simpr 486	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = ℕ → 𝐵 = ℕ)
53	52	eqcomd 2739	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ℕ → ℕ = 𝐵)
54	53	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
55	51, 54	eleqtrd 2836	. . . . . . . . . . . 12 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
56	55	adantll 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
57	50, 56	ffvelcdmd 7088	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑌)
58		eqid 2733	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))
59	57, 58	fmptd 7114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)
60	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)))
61	55	iftrued 4537	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
62	61	mpteq2dva 5249	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
63	60, 62	eqtrd 2773	. . . . . . . . . . 11 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
64	63	feq1d 6703	. . . . . . . . . 10 ⊢ (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
65	64	adantl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
66	59, 65	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67		f1ofo 6841	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵–onto→𝑌)
68	4, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐵–onto→𝑌)
69		dffo3 7104	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–onto→𝑌 ↔ (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
70	68, 69	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
71	70	simprd 497	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
72	71	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
73		simpr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
74		rspa 3246	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
75	72, 73, 74	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
76	75	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
77		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ 𝐵 = ℕ)
78		nfre1 3283	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)
79		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵)
80		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝐵 = ℕ)
81	79, 80	eleqtrd 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
82	81	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
83	82	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑛 ∈ ℕ)
84	60	fveq1d 6894	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = ℕ → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
85	84	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
86		fvex 6905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
87	86, 15	ifex 4579	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
89		eqid 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
90	89	fvmpt2 7010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
91	81, 88, 90	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
92	2	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
93	91, 92	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
94	93	3adant3 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
95		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝐹‘𝑛) → 𝑦 = (𝐹‘𝑛))
96	95	eqcomd 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐹‘𝑛) → (𝐹‘𝑛) = 𝑦)
97	96	3ad2ant3 1136	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐹‘𝑛) = 𝑦)
98	85, 94, 97	3eqtrrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
99	98	3adant1l 1177	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
100		rspe 3247	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
101	83, 99, 100	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
102	101	3exp 1120	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ 𝐵 → (𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
103	77, 78, 102	rexlimd 3264	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
104	103	adantr 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
105	76, 104	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
106	105	ralrimiva 3147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
107	66, 106	jca 513	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
108		dffo3 7104	. . . . . . 7 ⊢ (𝐴:ℕ–onto→𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
109	107, 108	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ–onto→𝑌)
110		founiiun 43875	. . . . . 6 ⊢ (𝐴:ℕ–onto→𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
111	109, 110	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
112		uniun 4935	. . . . . . . 8 ⊢ ∪ (𝑌 ∪ {∅}) = (∪ 𝑌 ∪ ∪ {∅})
113	15	unisn 4931	. . . . . . . . 9 ⊢ ∪ {∅} = ∅
114	113	uneq2i 4161	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∪ {∅}) = (∪ 𝑌 ∪ ∅)
115		un0 4391	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∅) = ∪ 𝑌
116	112, 114, 115	3eqtrri 2766	. . . . . . 7 ⊢ ∪ 𝑌 = ∪ (𝑌 ∪ {∅})
117	116	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ (𝑌 ∪ {∅}))
118	24	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120		isomenndlem.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℕ)
121	120	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
122	52	necon3bi 2968	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝐵 = ℕ → 𝐵 ≠ ℕ)
123	122	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124	121, 123	jca 513	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125		df-pss 3968	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126	124, 125	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127		pssnel 4471	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
128	126, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
129	128	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
130		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
131		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
132	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
133	23	fvmpt2 7010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
134	131, 132, 133	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
135	134	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
136	13	ad2antll 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
137		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
138	137	eqcomd 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
139	138	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∅ = 𝑦)
140	135, 136, 139	3eqtrrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑦 = (𝐴‘𝑛))
141	130, 140, 100	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
142	141	ex 414	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
143	142	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
144	119, 78, 129, 143	exlimimdd 2213	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
145	144	adantlr 714	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
146		simplll 774	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147		simpl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148		elsni 4646	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
149	148	con3i 154	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150	149	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151		elunnel2 4151	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦 ∈ 𝑌)
152	147, 150, 151	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
153	152	adantll 713	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
154	68	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐵–onto→𝑌)
155		foelcdmi 6954	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–onto→𝑌 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
156	154, 73, 155	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
157		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑦 ∈ 𝑌)
158	120	sselda 3983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
159	158	3adant3 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160	158, 87, 133	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
161	160, 3	eqtrd 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = (𝐹‘𝑛))
162	161	3adant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐴‘𝑛) = (𝐹‘𝑛))
163		simp3 1139	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐹‘𝑛) = 𝑦)
164	162, 163	eqtr2d 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑦 = (𝐴‘𝑛))
165	159, 164, 100	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
166	165	3exp 1120	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
167	166	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
168	157, 78, 167	rexlimd 3264	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
169	156, 168	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
170	146, 153, 169	syl2anc 585	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
171	145, 170	pm2.61dan 812	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
172	171	ralrimiva 3147	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
173	118, 172	jca 513	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
174		dffo3 7104	. . . . . . . 8 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
175	173, 174	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176		founiiun 43875	. . . . . . 7 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
177	175, 176	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
178	117, 177	eqtrd 2773	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
179	111, 178	pm2.61dan 812	. . . 4 ⊢ (𝜑 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
180	179	fveq2d 6896	. . 3 ⊢ (𝜑 → (𝑂‘∪ 𝑌) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
181		uncom 4154	. . . . . . . . 9 ⊢ ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182	181	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183		undif 4482	. . . . . . . . 9 ⊢ (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184	120, 183	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185	182, 184	eqtrd 2773	. . . . . . 7 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186	185	eqcomd 2739	. . . . . 6 ⊢ (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187	186	mpteq1d 5244	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))))
188	187	fveq2d 6896	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))))
189		nfv 1918	. . . . 5 ⊢ Ⅎ𝑛𝜑
190		difexg 5328	. . . . . . 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 5325	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
195		disjdifr 4473	. . . . . 6 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
196	195	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
197		simpl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
198		eldifi 4127	. . . . . . 7 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
199	198	adantl 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
200		isomenndlem.o	. . . . . . . 8 ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
201	200	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
202	31	ffvelcdmda 7087	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
203	201, 202	ffvelcdmd 7088	. . . . . 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 45127	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
207		eqid 2733	. . . . . . . 8 ⊢ (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))
208	205, 207	fmptd 7114	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))):𝐵⟶(0[,]+∞))
209	194, 208	sge0xrcl 45101	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) ∈ ℝ^*)
210	209	xaddlidd 44029	. . . . 5 ⊢ (𝜑 → (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
211	87	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
212	199, 211, 133	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
213		eldifn 4128	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛 ∈ 𝐵)
214	213	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛 ∈ 𝐵)
215	214	iffalsed 4540	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
216	212, 215	eqtrd 2773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = ∅)
217	216	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = (𝑂‘∅))
218		isomenndlem.o0	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∅) = 0)
219	197, 218	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
220	217, 219	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = 0)
221	220	mpteq2dva 5249	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
222	221	fveq2d 6896	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
223	189, 192	sge0z 45091	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
224	222, 223	eqtrd 2773	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = 0)
225	224	oveq1d 7424	. . . . 5 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
226	200, 25	feqresmpt 6962	. . . . . . 7 ⊢ (𝜑 → (𝑂 ↾ 𝑌) = (𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦)))
227	226	fveq2d 6896	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))))
228		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
229		fveq2 6892	. . . . . . 7 ⊢ (𝑦 = (𝐴‘𝑛) → (𝑂‘𝑦) = (𝑂‘(𝐴‘𝑛)))
230	161	eqcomd 2739	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = (𝐴‘𝑛))
231	200	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
232	25	sselda 3983	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝒫 𝑋)
233	231, 232	ffvelcdmd 7088	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑂‘𝑦) ∈ (0[,]+∞))
234	228, 189, 229, 194, 4, 230, 233	sge0f1o 45098	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
235		eqidd 2734	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
236	227, 234, 235	3eqtrd 2777	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
237	210, 225, 236	3eqtr4d 2783	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑂 ↾ 𝑌)))
238	188, 206, 237	3eqtrrd 2778	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
239	180, 238	breq12d 5162	. 2 ⊢ (𝜑 → ((𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
240	49, 239	mpbird 257	1 ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∖ cdif 3946 ∪ cun 3947 ∩ cin 3948 ⊆ wss 3949 ⊊ wpss 3950 ∅c0 4323 ifcif 4529 𝒫 cpw 4603 {csn 4629 ∪ cuni 4909 ∪ ciun 4998 class class class wbr 5149 ↦ cmpt 5232 ↾ cres 5679 ⟶wf 6540 –onto→wfo 6542 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 0cc0 11110 +∞cpnf 11245 ≤ cle 11249 ℕcn 12212 +_𝑒 cxad 13090 [,]cicc 13327 Σ^{^}csumge0 45078

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9437 df-oi 9505 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-n0 12473 df-z 12559 df-uz 12823 df-rp 12975 df-xadd 13093 df-ico 13330 df-icc 13331 df-fz 13485 df-fzo 13628 df-seq 13967 df-exp 14028 df-hash 14291 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-clim 15432 df-sum 15633 df-sumge0 45079

This theorem is referenced by: isomennd 45247

W3C validator