Theorem wunex2 9439

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𝑜)) ↾ ω)
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 2680	. . . . . . 7 ⊢ (𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran 𝐹)
3		frfnom 7417	. . . . . . . . 9 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω
4		wunex2.f	. . . . . . . . . 10 ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)
5	4	fneq1i 5899	. . . . . . . . 9 ⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω)
6	3, 5	mpbir 220	. . . . . . . 8 ⊢ 𝐹 Fn ω
7		fnunirn 6415	. . . . . . . 8 ⊢ (𝐹 Fn ω → (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
9	2, 8	bitri 263	. . . . . 6 ⊢ (𝑎 ∈ 𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
10		elssuni 4403	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
11	10	ad2antll 761	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
12		ssun2 3739	. . . . . . . . . . 11 ⊢ ∪ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
13		ssun1 3738	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
14	12, 13	sstri 3577	. . . . . . . . . 10 ⊢ ∪ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
15	11, 14	syl6ss 3580	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
16		simprl 790	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑚 ∈ ω)
17		fvex 6113	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑚) ∈ V
18	17	uniex 6851	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑚) ∈ V
19	17, 18	unex 6854	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∈ V
20		prex 4836	. . . . . . . . . . . . 13 ⊢ {𝒫 𝑢, ∪ 𝑢} ∈ V
21	17	mptex 6390	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
22	21	rnex 6992	. . . . . . . . . . . . 13 ⊢ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
23	20, 22	unex 6854	. . . . . . . . . . . 12 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
24	17, 23	iunex 7039	. . . . . . . . . . 11 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
25	19, 24	unex 6854	. . . . . . . . . 10 ⊢ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
27		unieq 4380	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧)
28	26, 27	uneq12d 3730	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧))
29		pweq 4111	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30		unieq 4380	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥)
31	29, 30	preq12d 4220	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪ 𝑥})
32		preq2 4213	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
33	32	cbvmptv 4678	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦})
34		preq1 4212	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
35	34	mpteq2dv 4673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
36	33, 35	syl5eq 2656	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
37	36	rneqd 5274	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
38	31, 37	uneq12d 3730	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})))
39	38	cbviunv 4495	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
40		mpteq1 4665	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
41	40	rneqd 5274	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
42	41	uneq2d 3729	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
43	26, 42	iuneq12d 4482	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
44	39, 43	syl5eq 2656	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
45	28, 44	uneq12d 3730	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))))
46		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → 𝑤 = (𝐹‘𝑚))
47		unieq 4380	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑤 = ∪ (𝐹‘𝑚))
48	46, 47	uneq12d 3730	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)))
49		mpteq1 4665	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
50	49	rneqd 5274	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐹‘𝑚) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
51	50	uneq2d 3729	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
52	46, 51	iuneq12d 4482	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
53	48, 52	uneq12d 3730	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑚) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
54	4, 45, 53	frsucmpt2 7422	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
55	16, 25, 54	sylancl 693	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
56	15, 55	sseqtr4d 3605	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57		fvssunirn 6127	. . . . . . . . 9 ⊢ (𝐹‘suc 𝑚) ⊆ ∪ ran 𝐹
58	57, 1	sseqtr4i 3601	. . . . . . . 8 ⊢ (𝐹‘suc 𝑚) ⊆ 𝑈
59	56, 58	syl6ss 3580	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ 𝑈)
60	59	rexlimdvaa 3014	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ 𝑈))
61	9, 60	syl5bi 231	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈))
62	61	ralrimiv 2948	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
63		dftr3 4684	. . . 4 ⊢ (Tr 𝑈 ↔ ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
64	62, 63	sylibr 223	. . 3 ⊢ (𝐴 ∈ 𝑉 → Tr 𝑈)
65		1on 7454	. . . . . . . 8 ⊢ 1𝑜 ∈ On
66		unexg 6857	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 1𝑜 ∈ On) → (𝐴 ∪ 1𝑜) ∈ V)
67	65, 66	mpan2 703	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1𝑜) ∈ V)
68	4	fveq1i 6104	. . . . . . . 8 ⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅)
69		fr0g 7418	. . . . . . . 8 ⊢ ((𝐴 ∪ 1𝑜) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅) = (𝐴 ∪ 1𝑜))
70	68, 69	syl5eq 2656	. . . . . . 7 ⊢ ((𝐴 ∪ 1𝑜) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
71	67, 70	syl 17	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
72		fvssunirn 6127	. . . . . . 7 ⊢ (𝐹‘∅) ⊆ ∪ ran 𝐹
73	72, 1	sseqtr4i 3601	. . . . . 6 ⊢ (𝐹‘∅) ⊆ 𝑈
74	71, 73	syl6eqssr 3619	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1𝑜) ⊆ 𝑈)
75	74	unssbd 3753	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 1𝑜 ⊆ 𝑈)
76		1n0 7462	. . . 4 ⊢ 1𝑜 ≠ ∅
77		ssn0 3928	. . . 4 ⊢ ((1𝑜 ⊆ 𝑈 ∧ 1𝑜 ≠ ∅) → 𝑈 ≠ ∅)
78	75, 76, 77	sylancl 693	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ≠ ∅)
79		pweq 4111	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80		unieq 4380	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
81	79, 80	preq12d 4220	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑎, ∪ 𝑎})
82		preq1 4212	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
83	82	mpteq2dv 4673	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
84	83	rneqd 5274	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
85	81, 84	uneq12d 3730	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})))
86	85	ssiun2s 4500	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐹‘𝑚) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
87	86	ad2antll 761	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
88		ssun2 3739	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
89	88, 55	syl5sseqr 3617	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
90	89, 58	syl6ss 3580	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
91	87, 90	sstrd 3578	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
92	91	unssad 3752	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
93		vpwex 4775	. . . . . . . . . 10 ⊢ 𝒫 𝑎 ∈ V
94		vuniex 6852	. . . . . . . . . 10 ⊢ ∪ 𝑎 ∈ V
95	93, 94	prss 4291	. . . . . . . . 9 ⊢ ((𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈) ↔ {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
96	92, 95	sylibr 223	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈))
97	96	simprd 478	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑎 ∈ 𝑈)
98	96	simpld 474	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝒫 𝑎 ∈ 𝑈)
99	1	eleq2i 2680	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran 𝐹)
100		fnunirn 6415	. . . . . . . . . . 11 ⊢ (𝐹 Fn ω → (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)))
101	6, 100	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
102	99, 101	bitri 263	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
103		simplrl 796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑚 ∈ ω)
104		simprl 790	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑛 ∈ ω)
105		ordom 6966	. . . . . . . . . . . . . . . . . 18 ⊢ Ord ω
106		ordunel 6919	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω)
107	105, 106	mp3an1 1403	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω)
108	103, 104, 107	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝑚 ∪ 𝑛) ∈ ω)
109		ssun1 3738	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛)
110		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
111	110	sseq2d 3596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑚)))
112		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
113	112	sseq2d 3596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑖)))
114		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = suc 𝑖 → (𝐹‘𝑘) = (𝐹‘suc 𝑖))
115	114	sseq2d 3596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = suc 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
116		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → (𝐹‘𝑘) = (𝐹‘(𝑚 ∪ 𝑛)))
117	116	sseq2d 3596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
118		ssid 3587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑚) ⊆ (𝐹‘𝑚)
119	118	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘𝑚))
120		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖))
121		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
122	121	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
123	120, 122	sseq12d 3597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)))
124		ssun1 3738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
125	124, 13	sstri 3577	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
126	25, 54	mpan2 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
127	125, 126	syl5sseqr 3617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚))
128	123, 127	vtoclga 3245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ω → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
129	128	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
130		sstr2 3575	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → ((𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
131	129, 130	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
132	111, 113, 115, 117, 119, 131	findsg 6985	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚 ∪ 𝑛)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
133	109, 132	mpan2 703	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
134	108, 103, 133	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
135		simplrr 797	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘𝑚))
136	134, 135	sseldd 3569	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
137	82	mpteq2dv 4673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
138	137	rneqd 5274	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
139	81, 138	uneq12d 3730	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})))
140	139	ssiun2s 4500	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
141	136, 140	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
142		ssun2 3739	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
143		fvex 6113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
144	143	uniex 6851	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
145	143, 144	unex 6854	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∈ V
146	143	mptex 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
147	146	rnex 6992	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
148	20, 147	unex 6854	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
149	143, 148	iunex 7039	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
150	145, 149	unex 6854	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
151		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → 𝑤 = (𝐹‘(𝑚 ∪ 𝑛)))
152		unieq 4380	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑤 = ∪ (𝐹‘(𝑚 ∪ 𝑛)))
153	151, 152	uneq12d 3730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))))
154		mpteq1 4665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
155	154	rneqd 5274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
156	155	uneq2d 3729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
157	151, 156	iuneq12d 4482	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
158	153, 157	uneq12d 3730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
159	4, 45, 158	frsucmpt2 7422	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
160	108, 150, 159	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
161	142, 160	syl5sseqr 3617	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚 ∪ 𝑛)))
162		fvssunirn 6127	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ ran 𝐹
163	162, 1	sseqtr4i 3601	. . . . . . . . . . . . . 14 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ 𝑈
164	161, 163	syl6ss 3580	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
165	141, 164	sstrd 3578	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
166	165	unssbd 3753	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
167		ssun2 3739	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛)
168		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑖 = (𝑚 ∪ 𝑛))
169	167, 168	syl5sseqr 3617	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑛 ⊆ 𝑖)
170	169	biantrud 527	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖)))
171	170	bicomd 212	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) ↔ 𝑛 ∈ ω))
172		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝐹‘𝑖) = (𝐹‘(𝑚 ∪ 𝑛)))
173	172	sseq2d 3596	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
174	171, 173	imbi12d 333	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) ↔ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))))
175		eleq1 2676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
176	175	anbi2d 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
177		sseq1 3589	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖))
178	176, 177	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖)))
179		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
180	179	sseq1d 3595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
181	178, 180	imbi12d 333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))))
182	111, 113, 115, 113, 119, 131	findsg 6985	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖))
183	181, 182	chvarv 2251	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))
184	183	expl 646	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
185	174, 184	vtoclga 3245	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∪ 𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
186	108, 104, 185	sylc 63	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
187		simprr 792	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘𝑛))
188	186, 187	sseldd 3569	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
189		prex 4836	. . . . . . . . . . . 12 ⊢ {𝑎, 𝑏} ∈ V
190		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})
191		preq2 4213	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
192	190, 191	elrnmpt1s 5294	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
193	188, 189, 192	sylancl 693	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
194	166, 193	sseldd 3569	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
195	194	rexlimdvaa 3014	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛) → {𝑎, 𝑏} ∈ 𝑈))
196	102, 195	syl5bi 231	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝑏 ∈ 𝑈 → {𝑎, 𝑏} ∈ 𝑈))
197	196	ralrimiv 2948	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)
198	97, 98, 197	3jca 1235	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
199	198	rexlimdvaa 3014	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
200	9, 199	syl5bi 231	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
201	200	ralrimiv 2948	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
202		rdgfun 7399	. . . . . . . . 9 ⊢ Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜))
203		omex 8423	. . . . . . . . 9 ⊢ ω ∈ V
204		resfunexg 6384	. . . . . . . . 9 ⊢ ((Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) ∈ V)
205	202, 203, 204	mp2an 704	. . . . . . . 8 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) ∈ V
206	4, 205	eqeltri 2684	. . . . . . 7 ⊢ 𝐹 ∈ V
207	206	rnex 6992	. . . . . 6 ⊢ ran 𝐹 ∈ V
208	207	uniex 6851	. . . . 5 ⊢ ∪ ran 𝐹 ∈ V
209	1, 208	eqeltri 2684	. . . 4 ⊢ 𝑈 ∈ V
210		iswun 9405	. . . 4 ⊢ (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))))
211	209, 210	ax-mp 5	. . 3 ⊢ (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
212	64, 78, 201, 211	syl3anbrc 1239	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ∈ WUni)
213	74	unssad 3752	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈)
214	212, 213	jca 553	1 ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {cpr 4127  ∪ cuni 4372  ∪ ciun 4455   ↦ cmpt 4643  Tr wtr 4680  ran crn 5039   ↾ cres 5040  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804  ωcom 6957  reccrdg 7392  1_𝑜c1o 7440  WUnicwun 9401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-wun 9403

This theorem is referenced by:  wunex  9440  wuncval2  9448