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 10778

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 2833	. . . . . . 7 ⊢ (𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran 𝐹)
3		frfnom 8475	. . . . . . . . 9 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω
4		wunex2.f	. . . . . . . . . 10 ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)
5	4	fneq1i 6665	. . . . . . . . 9 ⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω)
6	3, 5	mpbir 231	. . . . . . . 8 ⊢ 𝐹 Fn ω
7		fnunirn 7274	. . . . . . . 8 ⊢ (𝐹 Fn ω → (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
9	2, 8	bitri 275	. . . . . 6 ⊢ (𝑎 ∈ 𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
10		elssuni 4937	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
11	10	ad2antll 729	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
12		ssun2 4179	. . . . . . . . . . 11 ⊢ ∪ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
13		ssun1 4178	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
14	12, 13	sstri 3993	. . . . . . . . . 10 ⊢ ∪ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
15	11, 14	sstrdi 3996	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
16		simprl 771	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑚 ∈ ω)
17		fvex 6919	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑚) ∈ V
18	17	uniex 7761	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑚) ∈ V
19	17, 18	unex 7764	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∈ V
20		prex 5437	. . . . . . . . . . . . 13 ⊢ {𝒫 𝑢, ∪ 𝑢} ∈ V
21	17	mptex 7243	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
22	21	rnex 7932	. . . . . . . . . . . . 13 ⊢ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
23	20, 22	unex 7764	. . . . . . . . . . . 12 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
24	17, 23	iunex 7993	. . . . . . . . . . 11 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
25	19, 24	unex 7764	. . . . . . . . . 10 ⊢ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
27		unieq 4918	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧)
28	26, 27	uneq12d 4169	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧))
29		pweq 4614	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30		unieq 4918	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥)
31	29, 30	preq12d 4741	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪ 𝑥})
32		preq2 4734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
33	32	cbvmptv 5255	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦})
34		preq1 4733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
35	34	mpteq2dv 5244	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
36	33, 35	eqtrid 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
37	36	rneqd 5949	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
38	31, 37	uneq12d 4169	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})))
39	38	cbviunv 5040	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
40		mpteq1 5235	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
41	40	rneqd 5949	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
42	41	uneq2d 4168	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
43	26, 42	iuneq12d 5021	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
44	39, 43	eqtrid 2789	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
45	28, 44	uneq12d 4169	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))))
46		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → 𝑤 = (𝐹‘𝑚))
47		unieq 4918	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑤 = ∪ (𝐹‘𝑚))
48	46, 47	uneq12d 4169	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)))
49		mpteq1 5235	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
50	49	rneqd 5949	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐹‘𝑚) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
51	50	uneq2d 4168	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
52	46, 51	iuneq12d 5021	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
53	48, 52	uneq12d 4169	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑚) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
54	4, 45, 53	frsucmpt2 8480	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
55	16, 25, 54	sylancl 586	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
56	15, 55	sseqtrrd 4021	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57		fvssunirn 6939	. . . . . . . . 9 ⊢ (𝐹‘suc 𝑚) ⊆ ∪ ran 𝐹
58	57, 1	sseqtrri 4033	. . . . . . . 8 ⊢ (𝐹‘suc 𝑚) ⊆ 𝑈
59	56, 58	sstrdi 3996	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ 𝑈)
60	59	rexlimdvaa 3156	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ 𝑈))
61	9, 60	biimtrid 242	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈))
62	61	ralrimiv 3145	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
63		dftr3 5265	. . . 4 ⊢ (Tr 𝑈 ↔ ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
64	62, 63	sylibr 234	. . 3 ⊢ (𝐴 ∈ 𝑉 → Tr 𝑈)
65		1on 8518	. . . . . . . 8 ⊢ 1_o ∈ On
66		unexg 7763	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 1_o ∈ On) → (𝐴 ∪ 1_o) ∈ V)
67	65, 66	mpan2 691	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ∈ V)
68	4	fveq1i 6907	. . . . . . . 8 ⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅)
69		fr0g 8476	. . . . . . . 8 ⊢ ((𝐴 ∪ 1_o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅) = (𝐴 ∪ 1_o))
70	68, 69	eqtrid 2789	. . . . . . 7 ⊢ ((𝐴 ∪ 1_o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1_o))
71	67, 70	syl 17	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1_o))
72		fvssunirn 6939	. . . . . . 7 ⊢ (𝐹‘∅) ⊆ ∪ ran 𝐹
73	72, 1	sseqtrri 4033	. . . . . 6 ⊢ (𝐹‘∅) ⊆ 𝑈
74	71, 73	eqsstrrdi 4029	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ⊆ 𝑈)
75	74	unssbd 4194	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 1_o ⊆ 𝑈)
76		1n0 8526	. . . 4 ⊢ 1_o ≠ ∅
77		ssn0 4404	. . . 4 ⊢ ((1_o ⊆ 𝑈 ∧ 1_o ≠ ∅) → 𝑈 ≠ ∅)
78	75, 76, 77	sylancl 586	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ≠ ∅)
79		pweq 4614	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80		unieq 4918	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
81	79, 80	preq12d 4741	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑎, ∪ 𝑎})
82		preq1 4733	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
83	82	mpteq2dv 5244	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
84	83	rneqd 5949	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
85	81, 84	uneq12d 4169	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})))
86	85	ssiun2s 5048	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐹‘𝑚) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
87	86	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
88		ssun2 4179	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
89	88, 55	sseqtrrid 4027	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
90	89, 58	sstrdi 3996	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
91	87, 90	sstrd 3994	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
92	91	unssad 4193	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
93		vpwex 5377	. . . . . . . . . 10 ⊢ 𝒫 𝑎 ∈ V
94		vuniex 7759	. . . . . . . . . 10 ⊢ ∪ 𝑎 ∈ V
95	93, 94	prss 4820	. . . . . . . . 9 ⊢ ((𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈) ↔ {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
96	92, 95	sylibr 234	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈))
97	96	simprd 495	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑎 ∈ 𝑈)
98	96	simpld 494	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝒫 𝑎 ∈ 𝑈)
99	1	eleq2i 2833	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran 𝐹)
100		fnunirn 7274	. . . . . . . . . . 11 ⊢ (𝐹 Fn ω → (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)))
101	6, 100	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
102	99, 101	bitri 275	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
103		ordom 7897	. . . . . . . . . . . . . . . . 17 ⊢ Ord ω
104		simplrl 777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑚 ∈ ω)
105		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑛 ∈ ω)
106		ordunel 7847	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω)
107	103, 104, 105, 106	mp3an2i 1468	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝑚 ∪ 𝑛) ∈ ω)
108		ssun1 4178	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛)
109		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
110	109	sseq2d 4016	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑚)))
111		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
112	111	sseq2d 4016	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑖)))
113		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = suc 𝑖 → (𝐹‘𝑘) = (𝐹‘suc 𝑖))
114	113	sseq2d 4016	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = suc 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
115		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → (𝐹‘𝑘) = (𝐹‘(𝑚 ∪ 𝑛)))
116	115	sseq2d 4016	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
117		ssidd 4007	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘𝑚))
118		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖))
119		suceq 6450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
120	119	fveq2d 6910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
121	118, 120	sseq12d 4017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)))
122		ssun1 4178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
123	122, 13	sstri 3993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
124	25, 54	mpan2 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
125	123, 124	sseqtrrid 4027	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚))
126	121, 125	vtoclga 3577	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ω → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
127	126	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
128		sstr2 3990	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → ((𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
129	127, 128	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
130	110, 112, 114, 116, 117, 129	findsg 7919	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚 ∪ 𝑛)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
131	108, 130	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
132	107, 104, 131	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
133		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘𝑚))
134	132, 133	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
135	82	mpteq2dv 5244	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
136	135	rneqd 5949	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
137	81, 136	uneq12d 4169	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})))
138	137	ssiun2s 5048	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
139	134, 138	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
140		ssun2 4179	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
141		fvex 6919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
142	141	uniex 7761	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
143	141, 142	unex 7764	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∈ V
144	141	mptex 7243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
145	144	rnex 7932	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
146	20, 145	unex 7764	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
147	141, 146	iunex 7993	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
148	143, 147	unex 7764	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
149		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → 𝑤 = (𝐹‘(𝑚 ∪ 𝑛)))
150		unieq 4918	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑤 = ∪ (𝐹‘(𝑚 ∪ 𝑛)))
151	149, 150	uneq12d 4169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))))
152		mpteq1 5235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
153	152	rneqd 5949	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
154	153	uneq2d 4168	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
155	149, 154	iuneq12d 5021	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
156	151, 155	uneq12d 4169	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
157	4, 45, 156	frsucmpt2 8480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
158	107, 148, 157	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
159	140, 158	sseqtrrid 4027	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚 ∪ 𝑛)))
160		fvssunirn 6939	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ ran 𝐹
161	160, 1	sseqtrri 4033	. . . . . . . . . . . . . 14 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ 𝑈
162	159, 161	sstrdi 3996	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
163	139, 162	sstrd 3994	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
164	163	unssbd 4194	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
165		ssun2 4179	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛)
166		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑖 = (𝑚 ∪ 𝑛))
167	165, 166	sseqtrrid 4027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑛 ⊆ 𝑖)
168	167	biantrud 531	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖)))
169	168	bicomd 223	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) ↔ 𝑛 ∈ ω))
170		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝐹‘𝑖) = (𝐹‘(𝑚 ∪ 𝑛)))
171	170	sseq2d 4016	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
172	169, 171	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) ↔ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))))
173		eleq1w 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
174	173	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
175		sseq1 4009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖))
176	174, 175	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖)))
177		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
178	177	sseq1d 4015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
179	176, 178	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))))
180	110, 112, 114, 112, 117, 129	findsg 7919	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖))
181	179, 180	chvarvv 1998	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))
182	181	expl 457	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
183	172, 182	vtoclga 3577	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∪ 𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
184	107, 105, 183	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
185		simprr 773	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘𝑛))
186	184, 185	sseldd 3984	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
187		prex 5437	. . . . . . . . . . . 12 ⊢ {𝑎, 𝑏} ∈ V
188		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})
189		preq2 4734	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
190	188, 189	elrnmpt1s 5970	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
191	186, 187, 190	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
192	164, 191	sseldd 3984	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
193	192	rexlimdvaa 3156	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛) → {𝑎, 𝑏} ∈ 𝑈))
194	102, 193	biimtrid 242	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝑏 ∈ 𝑈 → {𝑎, 𝑏} ∈ 𝑈))
195	194	ralrimiv 3145	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)
196	97, 98, 195	3jca 1129	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
197	196	rexlimdvaa 3156	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
198	9, 197	biimtrid 242	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
199	198	ralrimiv 3145	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
200		rdgfun 8456	. . . . . . . . 9 ⊢ Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o))
201		omex 9683	. . . . . . . . 9 ⊢ ω ∈ V
202		resfunexg 7235	. . . . . . . . 9 ⊢ ((Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) ∈ V)
203	200, 201, 202	mp2an 692	. . . . . . . 8 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) ∈ V
204	4, 203	eqeltri 2837	. . . . . . 7 ⊢ 𝐹 ∈ V
205	204	rnex 7932	. . . . . 6 ⊢ ran 𝐹 ∈ V
206	205	uniex 7761	. . . . 5 ⊢ ∪ ran 𝐹 ∈ V
207	1, 206	eqeltri 2837	. . . 4 ⊢ 𝑈 ∈ V
208		iswun 10744	. . . 4 ⊢ (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))))
209	207, 208	ax-mp 5	. . 3 ⊢ (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
210	64, 78, 199, 209	syl3anbrc 1344	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ∈ WUni)
211	74	unssad 4193	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈)
212	210, 211	jca 511	1 ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ∪ cun 3949 ⊆ wss 3951 ∅c0 4333 𝒫 cpw 4600 {cpr 4628 ∪ cuni 4907 ∪ ciun 4991 ↦ cmpt 5225 Tr wtr 5259 ran crn 5686 ↾ cres 5687 Ord word 6383 Oncon0 6384 suc csuc 6386 Fun wfun 6555 Fn wfn 6556 ‘cfv 6561 ωcom 7887 reccrdg 8449 1_oc1o 8499 WUnicwun 10740

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-wun 10742

This theorem is referenced by: wunex 10779 wuncval2 10787

W3C validator