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 41264

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 4231	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
3	2	adantl 467	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
4		isomenndlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)
5		f1of 6278	. . . . . . . . . . 11 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵⟶𝑌)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐵⟶𝑌)
7		ssun1 3927	. . . . . . . . . . 11 ⊢ 𝑌 ⊆ (𝑌 ∪ {∅})
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ (𝑌 ∪ {∅}))
9	6, 8	fssd 6197	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐵⟶(𝑌 ∪ {∅}))
10	9	ffvelrnda 6502	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) ∈ (𝑌 ∪ {∅}))
11	3, 10	eqeltrd 2850	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
12	11	adantlr 694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13		iffalse 4234	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
14	13	adantl 467	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
15		0ex 4924	. . . . . . . . . . 11 ⊢ ∅ ∈ V
16	15	snid 4347	. . . . . . . . . 10 ⊢ ∅ ∈ {∅}
17		elun2 3932	. . . . . . . . . 10 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ∅ ∈ (𝑌 ∪ {∅})
19	18	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
20	14, 19	eqeltrd 2850	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
21	20	adantlr 694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
22	12, 21	pm2.61dan 814	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23		isomenndlem.a	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
24	22, 23	fmptd 6527	. . . 4 ⊢ (𝜑 → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
25		isomenndlem.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)
26		0elpw 4965	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑋
27		snssi 4474	. . . . . . 7 ⊢ (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
28	26, 27	ax-mp 5	. . . . . 6 ⊢ {∅} ⊆ 𝒫 𝑋
29	28	a1i 11	. . . . 5 ⊢ (𝜑 → {∅} ⊆ 𝒫 𝑋)
30	25, 29	unssd 3940	. . . 4 ⊢ (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
31	24, 30	fssd 6197	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 𝑋)
32		nnex 11228	. . . . . 6 ⊢ ℕ ∈ V
33	32	mptex 6630	. . . . 5 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ∈ V
34	23, 33	eqeltri 2846	. . . 4 ⊢ 𝐴 ∈ V
35		feq1 6166	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋 ↔ 𝐴:ℕ⟶𝒫 𝑋))
36	35	anbi2d 614	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋)))
37		fveq1 6331	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑎‘𝑛) = (𝐴‘𝑛))
38	37	iuneq2d 4681	. . . . . . 7 ⊢ (𝑎 = 𝐴 → ∪ 𝑛 ∈ ℕ (𝑎‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
39	38	fveq2d 6336	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
40		simpl 468	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → 𝑎 = 𝐴)
41	40	fveq1d 6334	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑎‘𝑛) = (𝐴‘𝑛))
42	41	fveq2d 6336	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝑎‘𝑛)) = (𝑂‘(𝐴‘𝑛)))
43	42	mpteq2dva 4878	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))
44	43	fveq2d 6336	. . . . . 6 ⊢ (𝑎 = 𝐴 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
45	39, 44	breq12d 4799	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
46	36, 45	imbi12d 333	. . . 4 ⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ↔ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))))
47		isomenndlem.subadd	. . . 4 ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))
48	34, 46, 47	vtocl 3410	. . 3 ⊢ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
49	1, 31, 48	syl2anc 573	. 2 ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
50	6	ad2antrr 705	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵⟶𝑌)
51		simpr 471	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = ℕ → 𝐵 = ℕ)
53	52	eqcomd 2777	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ℕ → ℕ = 𝐵)
54	53	adantr 466	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
55	51, 54	eleqtrd 2852	. . . . . . . . . . . 12 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
56	55	adantll 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵)
57	50, 56	ffvelrnd 6503	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑌)
58		eqid 2771	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))
59	57, 58	fmptd 6527	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)
60	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)))
61	55	iftrued 4233	. . . . . . . . . . . . 13 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
62	61	mpteq2dva 4878	. . . . . . . . . . . 12 ⊢ (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
63	60, 62	eqtrd 2805	. . . . . . . . . . 11 ⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)))
64	63	feq1d 6170	. . . . . . . . . 10 ⊢ (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
65	64	adantl 467	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌))
66	59, 65	mpbird 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67		f1ofo 6285	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵–onto→𝑌)
68	4, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐵–onto→𝑌)
69		dffo3 6517	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–onto→𝑌 ↔ (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
70	68, 69	sylib 208	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)))
71	70	simprd 483	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
72	71	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
73		simpr 471	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
74		rspa 3079	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
75	72, 73, 74	syl2anc 573	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
76	75	adantlr 694	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))
77		nfv 1995	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ 𝐵 = ℕ)
78		nfre1 3153	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)
79		simpr 471	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵)
80		simpl 468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝐵 = ℕ)
81	79, 80	eleqtrd 2852	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
82	81	adantll 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
83	82	3adant3 1126	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑛 ∈ ℕ)
84	60	fveq1d 6334	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = ℕ → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
85	84	3ad2ant1 1127	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛))
86		fvex 6342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
87	86, 15	ifex 4295	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
89		eqid 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
90	89	fvmpt2 6433	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
91	81, 88, 90	syl2anc 573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
92	2	adantl 467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛))
93	91, 92	eqtrd 2805	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
94	93	3adant3 1126	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛))
95		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝐹‘𝑛) → 𝑦 = (𝐹‘𝑛))
96	95	eqcomd 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐹‘𝑛) → (𝐹‘𝑛) = 𝑦)
97	96	3ad2ant3 1129	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐹‘𝑛) = 𝑦)
98	85, 94, 97	3eqtrrd 2810	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
99	98	3adant1l 1185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛))
100		rspe 3151	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
101	83, 99, 100	syl2anc 573	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
102	101	3exp 1112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ 𝐵 → (𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
103	77, 78, 102	rexlimd 3174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
104	103	adantr 466	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
105	76, 104	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
106	105	ralrimiva 3115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
107	66, 106	jca 501	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
108		dffo3 6517	. . . . . . 7 ⊢ (𝐴:ℕ–onto→𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
109	107, 108	sylibr 224	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ–onto→𝑌)
110		founiiun 39880	. . . . . 6 ⊢ (𝐴:ℕ–onto→𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
111	109, 110	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
112		uniun 4593	. . . . . . . 8 ⊢ ∪ (𝑌 ∪ {∅}) = (∪ 𝑌 ∪ ∪ {∅})
113	15	unisn 4589	. . . . . . . . 9 ⊢ ∪ {∅} = ∅
114	113	uneq2i 3915	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∪ {∅}) = (∪ 𝑌 ∪ ∅)
115		un0 4111	. . . . . . . 8 ⊢ (∪ 𝑌 ∪ ∅) = ∪ 𝑌
116	112, 114, 115	3eqtrri 2798	. . . . . . 7 ⊢ ∪ 𝑌 = ∪ (𝑌 ∪ {∅})
117	116	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ (𝑌 ∪ {∅}))
118	24	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119		isomenndlem.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℕ)
120	119	adantr 466	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
121	52	necon3bi 2969	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝐵 = ℕ → 𝐵 ≠ ℕ)
122	121	adantl 467	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
123	120, 122	jca 501	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
124		df-pss 3739	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125	123, 124	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
126		pssnel 4181	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
127	125, 126	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
128	127	adantr 466	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵))
129		nfv 1995	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
130		simprl 754	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
131		simprl 754	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ)
132	87	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
133	23	fvmpt2 6433	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
134	131, 132, 133	syl2anc 573	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
135	134	adantlr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
136	13	ad2antll 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
137		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
138	137	eqcomd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
139	138	ad2antlr 706	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∅ = 𝑦)
140	135, 136, 139	3eqtrrd 2810	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑦 = (𝐴‘𝑛))
141	130, 140, 100	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
142	141	ex 397	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
143	142	adantlr 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
144	129, 78, 143	exlimd 2243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → (∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
145	128, 144	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
146	145	adantlr 694	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
147		simplll 758	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
148		simpl 468	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
149		elsni 4333	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
150	149	con3i 151	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
151	150	adantl 467	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
152		elunnel2 39720	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦 ∈ 𝑌)
153	148, 151, 152	syl2anc 573	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
154	153	adantll 693	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌)
155	68	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐵–onto→𝑌)
156		foelrni 6386	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐵–onto→𝑌 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
157	155, 73, 156	syl2anc 573	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦)
158		nfv 1995	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑦 ∈ 𝑌)
159	119	sselda 3752	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ)
160	159	3adant3 1126	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑛 ∈ ℕ)
161	159, 87, 133	sylancl 574	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
162	161, 3	eqtrd 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = (𝐹‘𝑛))
163	162	3adant3 1126	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐴‘𝑛) = (𝐹‘𝑛))
164		simp3 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐹‘𝑛) = 𝑦)
165	163, 164	eqtr2d 2806	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑦 = (𝐴‘𝑛))
166	160, 165, 100	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
167	166	3exp 1112	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
168	167	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))))
169	158, 78, 168	rexlimd 3174	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
170	157, 169	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
171	147, 154, 170	syl2anc 573	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
172	146, 171	pm2.61dan 814	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
173	172	ralrimiva 3115	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))
174	118, 173	jca 501	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
175		dffo3 6517	. . . . . . . 8 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))
176	174, 175	sylibr 224	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
177		founiiun 39880	. . . . . . 7 ⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
178	176, 177	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ (𝑌 ∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
179	117, 178	eqtrd 2805	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
180	111, 179	pm2.61dan 814	. . . 4 ⊢ (𝜑 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛))
181	180	fveq2d 6336	. . 3 ⊢ (𝜑 → (𝑂‘∪ 𝑌) = (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)))
182		uncom 3908	. . . . . . . . 9 ⊢ ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
183	182	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
184		undif 4191	. . . . . . . . 9 ⊢ (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185	119, 184	sylib 208	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
186	183, 185	eqtrd 2805	. . . . . . 7 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
187	186	eqcomd 2777	. . . . . 6 ⊢ (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
188	187	mpteq1d 4872	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))))
189	188	fveq2d 6336	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))))
190		nfv 1995	. . . . 5 ⊢ Ⅎ𝑛𝜑
191		difexg 4942	. . . . . . 7 ⊢ (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
192	32, 191	ax-mp 5	. . . . . 6 ⊢ (ℕ ∖ 𝐵) ∈ V
193	192	a1i 11	. . . . 5 ⊢ (𝜑 → (ℕ ∖ 𝐵) ∈ V)
194	32	a1i 11	. . . . . 6 ⊢ (𝜑 → ℕ ∈ V)
195	194, 119	ssexd 4939	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
196		incom 3956	. . . . . . 7 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (ℕ ∖ 𝐵))
197		disjdif 4182	. . . . . . 7 ⊢ (𝐵 ∩ (ℕ ∖ 𝐵)) = ∅
198	196, 197	eqtri 2793	. . . . . 6 ⊢ ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
199	198	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
200		simpl 468	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
201		eldifi 3883	. . . . . . 7 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
202	201	adantl 467	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
203		isomenndlem.o	. . . . . . . 8 ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
204	203	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
205	31	ffvelrnda 6502	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
206	204, 205	ffvelrnd 6503	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
207	200, 202, 206	syl2anc 573	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
208	159, 206	syldan 579	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞))
209	190, 193, 195, 199, 207, 208	sge0splitmpt 41145	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
210		eqid 2771	. . . . . . . 8 ⊢ (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))
211	208, 210	fmptd 6527	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))):𝐵⟶(0[,]+∞))
212	195, 211	sge0xrcl 41119	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) ∈ ℝ^*)
213	212	xaddid2d 40051	. . . . 5 ⊢ (𝜑 → (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
214	87	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V)
215	202, 214, 133	syl2anc 573	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))
216		eldifn 3884	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛 ∈ 𝐵)
217	216	adantl 467	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛 ∈ 𝐵)
218	217	iffalsed 4236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅)
219	215, 218	eqtrd 2805	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = ∅)
220	219	fveq2d 6336	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = (𝑂‘∅))
221		isomenndlem.o0	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∅) = 0)
222	200, 221	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
223	220, 222	eqtrd 2805	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = 0)
224	223	mpteq2dva 4878	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
225	224	fveq2d 6336	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
226	190, 193	sge0z 41109	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
227	225, 226	eqtrd 2805	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = 0)
228	227	oveq1d 6808	. . . . 5 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (0 +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))))
229	203, 25	feqresmpt 6392	. . . . . . 7 ⊢ (𝜑 → (𝑂 ↾ 𝑌) = (𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦)))
230	229	fveq2d 6336	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))))
231		nfv 1995	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
232		fveq2 6332	. . . . . . 7 ⊢ (𝑦 = (𝐴‘𝑛) → (𝑂‘𝑦) = (𝑂‘(𝐴‘𝑛)))
233	162	eqcomd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = (𝐴‘𝑛))
234	203	adantr 466	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
235	25	sselda 3752	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝒫 𝑋)
236	234, 235	ffvelrnd 6503	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑂‘𝑦) ∈ (0[,]+∞))
237	231, 190, 232, 195, 4, 233, 236	sge0f1o 41116	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
238		eqidd 2772	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
239	230, 237, 238	3eqtrd 2809	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))
240	213, 228, 239	3eqtr4d 2815	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (Σ^{^}‘(𝑂 ↾ 𝑌)))
241	189, 209, 240	3eqtrrd 2810	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑂 ↾ 𝑌)) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))
242	181, 241	breq12d 4799	. 2 ⊢ (𝜑 → ((𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)) ↔ (𝑂‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))
243	49, 242	mpbird 247	1 ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^{^}‘(𝑂 ↾ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∃wex 1852 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∃wrex 3062 Vcvv 3351 ∖ cdif 3720 ∪ cun 3721 ∩ cin 3722 ⊆ wss 3723 ⊊ wpss 3724 ∅c0 4063 ifcif 4225 𝒫 cpw 4297 {csn 4316 ∪ cuni 4574 ∪ ciun 4654 class class class wbr 4786 ↦ cmpt 4863 ↾ cres 5251 ⟶wf 6027 –onto→wfo 6029 –1-1-onto→wf1o 6030 ‘cfv 6031 (class class class)co 6793 0cc0 10138 +∞cpnf 10273 ≤ cle 10277 ℕcn 11222 +_𝑒 cxad 12149 [,]cicc 12383 Σ^{^}csumge0 41096

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 ax-inf2 8702 ax-cnex 10194 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rnegex 10209 ax-rrecex 10210 ax-cnre 10211 ax-pre-lttri 10212 ax-pre-lttrn 10213 ax-pre-ltadd 10214 ax-pre-mulgt0 10215 ax-pre-sup 10216

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-se 5209 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-isom 6040 df-riota 6754 df-ov 6796 df-oprab 6797 df-mpt2 6798 df-om 7213 df-1st 7315 df-2nd 7316 df-wrecs 7559 df-recs 7621 df-rdg 7659 df-1o 7713 df-oadd 7717 df-er 7896 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-sup 8504 df-oi 8571 df-card 8965 df-pnf 10278 df-mnf 10279 df-xr 10280 df-ltxr 10281 df-le 10282 df-sub 10470 df-neg 10471 df-div 10887 df-nn 11223 df-2 11281 df-3 11282 df-n0 11495 df-z 11580 df-uz 11889 df-rp 12036 df-xadd 12152 df-ico 12386 df-icc 12387 df-fz 12534 df-fzo 12674 df-seq 13009 df-exp 13068 df-hash 13322 df-cj 14047 df-re 14048 df-im 14049 df-sqrt 14183 df-abs 14184 df-clim 14427 df-sum 14625 df-sumge0 41097

This theorem is referenced by: isomennd 41265

W3C validator