wunex2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wunex2		Structured version Visualization version GIF version

Theorem wunex2 10823

Description: Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)

**Hypotheses**
Ref	Expression
wunex2.f	⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)
wunex2.u	⊢ 𝑈 = ∪ ran 𝐹

**Assertion**
Ref	Expression
wunex2	⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))

Distinct variable group: 𝑥,𝑦,𝑧 Allowed substitution hints: 𝐴(𝑥, 𝑦, 𝑧) 𝑈(𝑥, 𝑦, 𝑧) 𝐹(𝑥, 𝑦, 𝑧) 𝑉(𝑥, 𝑦, 𝑧)

Proof of Theorem wunex2 Dummy variables 𝑢 𝑎 𝑣 𝑤 𝑏 𝑚 𝑛 𝑖 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wunex2.u	. . . . . . . 8 ⊢ 𝑈 = ∪ ran 𝐹
2	1	eleq2i 2853	. . . . . . 7 ⊢ (𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran 𝐹)
3		frfnom 8443	. . . . . . . . 9 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω
4		wunex2.f	. . . . . . . . . 10 ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)
5	4	fneq1i 6636	. . . . . . . . 9 ⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω)
6	3, 5	mpbir 234	. . . . . . . 8 ⊢ 𝐹 Fn ω
7		fnunirn 7257	. . . . . . . 8 ⊢ (𝐹 Fn ω → (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
9	2, 8	bitri 278	. . . . . 6 ⊢ (𝑎 ∈ 𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
10		elssuni 4899	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
11	10	ad2antll 742	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
12		ssun2 4125	. . . . . . . . . . 11 ⊢ ∪ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
13		ssun1 4124	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
14	12, 13	sstri 3940	. . . . . . . . . 10 ⊢ ∪ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
15	11, 14	sstrdi 3943	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
16		simprl 783	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑚 ∈ ω)
17		fvex 6898	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑚) ∈ V
18	17	uniex 7758	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑚) ∈ V
19	17, 18	unex 7761	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∈ V
20		prex 5396	. . . . . . . . . . . . 13 ⊢ {𝒫 𝑢, ∪ 𝑢} ∈ V
21	17	mptex 7229	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
22	21	rnex 7922	. . . . . . . . . . . . 13 ⊢ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
23	20, 22	unex 7761	. . . . . . . . . . . 12 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
24	17, 23	iunex 7980	. . . . . . . . . . 11 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
25	19, 24	unex 7761	. . . . . . . . . 10 ⊢ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26		id 23	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
27		unieq 4878	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧)
28	26, 27	uneq12d 4116	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧))
29		pweq 4571	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30		unieq 4878	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥)
31	29, 30	preq12d 4702	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪ 𝑥})
32		preq2 4695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
33	32	cbvmptv 5209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦})
34		preq1 4694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
35	34	mpteq2dv 5199	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
36	33, 35	eqtrid 2808	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
37	36	rneqd 5920	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
38	31, 37	uneq12d 4116	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})))
39	38	cbviunv 4997	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
40		mpteq1 5194	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
41	40	rneqd 5920	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
42	41	uneq2d 4115	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
43	26, 42	iuneq12d 4980	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
44	39, 43	eqtrid 2808	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
45	28, 44	uneq12d 4116	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))))
46		id 23	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → 𝑤 = (𝐹‘𝑚))
47		unieq 4878	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑤 = ∪ (𝐹‘𝑚))
48	46, 47	uneq12d 4116	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)))
49		mpteq1 5194	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
50	49	rneqd 5920	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐹‘𝑚) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
51	50	uneq2d 4115	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
52	46, 51	iuneq12d 4980	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
53	48, 52	uneq12d 4116	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑚) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
54	4, 45, 53	frsucmpt2 8448	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
55	16, 25, 54	sylancl 598	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
56	15, 55	sseqtrrd 3968	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57		fvssunirn 6916	. . . . . . . . 9 ⊢ (𝐹‘suc 𝑚) ⊆ ∪ ran 𝐹
58	57, 1	sseqtrri 3980	. . . . . . . 8 ⊢ (𝐹‘suc 𝑚) ⊆ 𝑈
59	56, 58	sstrdi 3943	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ 𝑈)
60	59	rexlimdvaa 3165	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ 𝑈))
61	9, 60	biimtrid 245	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈))
62	61	ralrimiv 3154	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
63		dftr3 5217	. . . 4 ⊢ (Tr 𝑈 ↔ ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
64	62, 63	sylibr 237	. . 3 ⊢ (𝐴 ∈ 𝑉 → Tr 𝑈)
65		1on 8489	. . . . . . . 8 ⊢ 1_o ∈ On
66		unexg 7760	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 1_o ∈ On) → (𝐴 ∪ 1_o) ∈ V)
67	65, 66	mpan2 704	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ∈ V)
68	4	fveq1i 6886	. . . . . . . 8 ⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅)
69		fr0g 8444	. . . . . . . 8 ⊢ ((𝐴 ∪ 1_o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅) = (𝐴 ∪ 1_o))
70	68, 69	eqtrid 2808	. . . . . . 7 ⊢ ((𝐴 ∪ 1_o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1_o))
71	67, 70	syl 18	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1_o))
72		fvssunirn 6916	. . . . . . 7 ⊢ (𝐹‘∅) ⊆ ∪ ran 𝐹
73	72, 1	sseqtrri 3980	. . . . . 6 ⊢ (𝐹‘∅) ⊆ 𝑈
74	71, 73	eqsstrrdi 3976	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ⊆ 𝑈)
75	74	unssbd 4140	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 1_o ⊆ 𝑈)
76		1n0 8495	. . . 4 ⊢ 1_o ≠ ∅
77		ssn0 4355	. . . 4 ⊢ ((1_o ⊆ 𝑈 ∧ 1_o ≠ ∅) → 𝑈 ≠ ∅)
78	75, 76, 77	sylancl 598	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ≠ ∅)
79		pweq 4571	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80		unieq 4878	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
81	79, 80	preq12d 4702	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑎, ∪ 𝑎})
82		preq1 4694	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
83	82	mpteq2dv 5199	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
84	83	rneqd 5920	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
85	81, 84	uneq12d 4116	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})))
86	85	ssiun2s 5007	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐹‘𝑚) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
87	86	ad2antll 742	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
88		ssun2 4125	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
89	88, 55	sseqtrrid 3974	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
90	89, 58	sstrdi 3943	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
91	87, 90	sstrd 3941	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
92	91	unssad 4139	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
93		vpwex 5339	. . . . . . . . . 10 ⊢ 𝒫 𝑎 ∈ V
94		vuniex 7756	. . . . . . . . . 10 ⊢ ∪ 𝑎 ∈ V
95	93, 94	prss 4781	. . . . . . . . 9 ⊢ ((𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈) ↔ {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
96	92, 95	sylibr 237	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈))
97	96	simprd 501	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑎 ∈ 𝑈)
98	96	simpld 500	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝒫 𝑎 ∈ 𝑈)
99	1	eleq2i 2853	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran 𝐹)
100		fnunirn 7257	. . . . . . . . . . 11 ⊢ (𝐹 Fn ω → (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)))
101	6, 100	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
102	99, 101	bitri 278	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
103		ordom 7887	. . . . . . . . . . . . . . . . 17 ⊢ Ord ω
104		simplrl 789	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑚 ∈ ω)
105		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑛 ∈ ω)
106		ordunel 7838	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω)
107	103, 104, 105, 106	mp3an2i 1495	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝑚 ∪ 𝑛) ∈ ω)
108		ssun1 4124	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛)
109		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
110	109	sseq2d 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑚)))
111		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
112	111	sseq2d 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑖)))
113		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = suc 𝑖 → (𝐹‘𝑘) = (𝐹‘suc 𝑖))
114	113	sseq2d 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = suc 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
115		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → (𝐹‘𝑘) = (𝐹‘(𝑚 ∪ 𝑛)))
116	115	sseq2d 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
117		ssidd 3954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘𝑚))
118		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖))
119		suceq 6431	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
120	119	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
121	118, 120	sseq12d 3964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)))
122		ssun1 4124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
123	122, 13	sstri 3940	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
124	25, 54	mpan2 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
125	123, 124	sseqtrrid 3974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚))
126	121, 125	vtoclga 3537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ω → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
127	126	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
128		sstr2 3938	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → ((𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
129	127, 128	syl5com 32	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
130	110, 112, 114, 116, 117, 129	findsg 7909	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚 ∪ 𝑛)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
131	108, 130	mpan2 704	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
132	107, 104, 131	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
133		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘𝑚))
134	132, 133	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
135	82	mpteq2dv 5199	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
136	135	rneqd 5920	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
137	81, 136	uneq12d 4116	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})))
138	137	ssiun2s 5007	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
139	134, 138	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
140		ssun2 4125	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
141		fvex 6898	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
142	141	uniex 7758	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
143	141, 142	unex 7761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∈ V
144	141	mptex 7229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
145	144	rnex 7922	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
146	20, 145	unex 7761	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
147	141, 146	iunex 7980	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
148	143, 147	unex 7761	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
149		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → 𝑤 = (𝐹‘(𝑚 ∪ 𝑛)))
150		unieq 4878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑤 = ∪ (𝐹‘(𝑚 ∪ 𝑛)))
151	149, 150	uneq12d 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))))
152		mpteq1 5194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
153	152	rneqd 5920	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
154	153	uneq2d 4115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
155	149, 154	iuneq12d 4980	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
156	151, 155	uneq12d 4116	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
157	4, 45, 156	frsucmpt2 8448	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
158	107, 148, 157	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
159	140, 158	sseqtrrid 3974	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚 ∪ 𝑛)))
160		fvssunirn 6916	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ ran 𝐹
161	160, 1	sseqtrri 3980	. . . . . . . . . . . . . 14 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ 𝑈
162	159, 161	sstrdi 3943	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
163	139, 162	sstrd 3941	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
164	163	unssbd 4140	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
165		ssun2 4125	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛)
166		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑖 = (𝑚 ∪ 𝑛))
167	165, 166	sseqtrrid 3974	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑛 ⊆ 𝑖)
168	167	biantrud 541	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖)))
169	168	bicomd 226	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) ↔ 𝑛 ∈ ω))
170		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝐹‘𝑖) = (𝐹‘(𝑚 ∪ 𝑛)))
171	170	sseq2d 3963	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
172	169, 171	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) ↔ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))))
173		eleq1w 2844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
174	173	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
175		sseq1 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖))
176	174, 175	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖)))
177		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
178	177	sseq1d 3962	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
179	176, 178	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))))
180	110, 112, 114, 112, 117, 129	findsg 7909	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖))
181	179, 180	chvarvv 2022	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))
182	181	expl 463	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
183	172, 182	vtoclga 3537	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∪ 𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
184	107, 105, 183	sylc 66	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
185		simprr 785	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘𝑛))
186	184, 185	sseldd 3932	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
187		prex 5396	. . . . . . . . . . . 12 ⊢ {𝑎, 𝑏} ∈ V
188		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})
189		preq2 4695	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
190	188, 189	elrnmpt1s 5941	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
191	186, 187, 190	sylancl 598	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
192	164, 191	sseldd 3932	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
193	192	rexlimdvaa 3165	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛) → {𝑎, 𝑏} ∈ 𝑈))
194	102, 193	biimtrid 245	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝑏 ∈ 𝑈 → {𝑎, 𝑏} ∈ 𝑈))
195	194	ralrimiv 3154	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)
196	97, 98, 195	3jca 1146	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
197	196	rexlimdvaa 3165	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
198	9, 197	biimtrid 245	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
199	198	ralrimiv 3154	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
200		rdgfun 8424	. . . . . . . . 9 ⊢ Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o))
201		omex 9644	. . . . . . . . 9 ⊢ ω ∈ V
202		resfunexg 7221	. . . . . . . . 9 ⊢ ((Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) ∈ V)
203	200, 201, 202	mp2an 705	. . . . . . . 8 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) ∈ V
204	4, 203	eqeltri 2857	. . . . . . 7 ⊢ 𝐹 ∈ V
205	204	rnex 7922	. . . . . 6 ⊢ ran 𝐹 ∈ V
206	205	uniex 7758	. . . . 5 ⊢ ∪ ran 𝐹 ∈ V
207	1, 206	eqeltri 2857	. . . 4 ⊢ 𝑈 ∈ V
208		iswun 10789	. . . 4 ⊢ (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))))
209	207, 208	ax-mp 5	. . 3 ⊢ (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
210	64, 78, 199, 209	syl3anbrc 1362	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ∈ WUni)
211	74	unssad 4139	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈)
212	210, 211	jca 521	1 ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 𝒫 cpw 4557 {cpr 4586 ∪ cuni 4867 ∪ ciun 4951 ↦ cmpt 5186 Tr wtr 5212 ran crn 5652 ↾ cres 5653 Ord word 6361 Oncon0 6362 suc csuc 6364 Fun wfun 6532 Fn wfn 6533 ‘cfv 6538 ωcom 7877 reccrdg 8417 1_oc1o 8469 WUnicwun 10785

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-inf2 9642

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-om 7878 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-wun 10787

This theorem is used by: wunex 10824 wuncval2 10832

W3C validator