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 10698

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 2821	. . . . . . 7 ⊢ (𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran 𝐹)
3		frfnom 8406	. . . . . . . . 9 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω
4		wunex2.f	. . . . . . . . . 10 ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)
5	4	fneq1i 6618	. . . . . . . . 9 ⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω)
6	3, 5	mpbir 231	. . . . . . . 8 ⊢ 𝐹 Fn ω
7		fnunirn 7231	. . . . . . . 8 ⊢ (𝐹 Fn ω → (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
9	2, 8	bitri 275	. . . . . 6 ⊢ (𝑎 ∈ 𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
10		elssuni 4904	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
11	10	ad2antll 729	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
12		ssun2 4145	. . . . . . . . . . 11 ⊢ ∪ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
13		ssun1 4144	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
14	12, 13	sstri 3959	. . . . . . . . . 10 ⊢ ∪ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
15	11, 14	sstrdi 3962	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
16		simprl 770	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑚 ∈ ω)
17		fvex 6874	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑚) ∈ V
18	17	uniex 7720	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑚) ∈ V
19	17, 18	unex 7723	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∈ V
20		prex 5395	. . . . . . . . . . . . 13 ⊢ {𝒫 𝑢, ∪ 𝑢} ∈ V
21	17	mptex 7200	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
22	21	rnex 7889	. . . . . . . . . . . . 13 ⊢ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
23	20, 22	unex 7723	. . . . . . . . . . . 12 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
24	17, 23	iunex 7950	. . . . . . . . . . 11 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
25	19, 24	unex 7723	. . . . . . . . . 10 ⊢ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
27		unieq 4885	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧)
28	26, 27	uneq12d 4135	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧))
29		pweq 4580	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30		unieq 4885	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥)
31	29, 30	preq12d 4708	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪ 𝑥})
32		preq2 4701	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
33	32	cbvmptv 5214	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦})
34		preq1 4700	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
35	34	mpteq2dv 5204	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
36	33, 35	eqtrid 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
37	36	rneqd 5905	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
38	31, 37	uneq12d 4135	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})))
39	38	cbviunv 5007	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
40		mpteq1 5199	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
41	40	rneqd 5905	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
42	41	uneq2d 4134	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
43	26, 42	iuneq12d 4988	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
44	39, 43	eqtrid 2777	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
45	28, 44	uneq12d 4135	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))))
46		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → 𝑤 = (𝐹‘𝑚))
47		unieq 4885	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑤 = ∪ (𝐹‘𝑚))
48	46, 47	uneq12d 4135	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)))
49		mpteq1 5199	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
50	49	rneqd 5905	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐹‘𝑚) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
51	50	uneq2d 4134	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
52	46, 51	iuneq12d 4988	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
53	48, 52	uneq12d 4135	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑚) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
54	4, 45, 53	frsucmpt2 8411	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
55	16, 25, 54	sylancl 586	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
56	15, 55	sseqtrrd 3987	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57		fvssunirn 6894	. . . . . . . . 9 ⊢ (𝐹‘suc 𝑚) ⊆ ∪ ran 𝐹
58	57, 1	sseqtrri 3999	. . . . . . . 8 ⊢ (𝐹‘suc 𝑚) ⊆ 𝑈
59	56, 58	sstrdi 3962	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ 𝑈)
60	59	rexlimdvaa 3136	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ 𝑈))
61	9, 60	biimtrid 242	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈))
62	61	ralrimiv 3125	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
63		dftr3 5223	. . . 4 ⊢ (Tr 𝑈 ↔ ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
64	62, 63	sylibr 234	. . 3 ⊢ (𝐴 ∈ 𝑉 → Tr 𝑈)
65		1on 8449	. . . . . . . 8 ⊢ 1_o ∈ On
66		unexg 7722	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 1_o ∈ On) → (𝐴 ∪ 1_o) ∈ V)
67	65, 66	mpan2 691	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ∈ V)
68	4	fveq1i 6862	. . . . . . . 8 ⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅)
69		fr0g 8407	. . . . . . . 8 ⊢ ((𝐴 ∪ 1_o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅) = (𝐴 ∪ 1_o))
70	68, 69	eqtrid 2777	. . . . . . 7 ⊢ ((𝐴 ∪ 1_o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1_o))
71	67, 70	syl 17	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1_o))
72		fvssunirn 6894	. . . . . . 7 ⊢ (𝐹‘∅) ⊆ ∪ ran 𝐹
73	72, 1	sseqtrri 3999	. . . . . 6 ⊢ (𝐹‘∅) ⊆ 𝑈
74	71, 73	eqsstrrdi 3995	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ⊆ 𝑈)
75	74	unssbd 4160	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 1_o ⊆ 𝑈)
76		1n0 8455	. . . 4 ⊢ 1_o ≠ ∅
77		ssn0 4370	. . . 4 ⊢ ((1_o ⊆ 𝑈 ∧ 1_o ≠ ∅) → 𝑈 ≠ ∅)
78	75, 76, 77	sylancl 586	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ≠ ∅)
79		pweq 4580	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80		unieq 4885	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
81	79, 80	preq12d 4708	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑎, ∪ 𝑎})
82		preq1 4700	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
83	82	mpteq2dv 5204	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
84	83	rneqd 5905	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
85	81, 84	uneq12d 4135	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})))
86	85	ssiun2s 5015	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐹‘𝑚) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
87	86	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
88		ssun2 4145	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
89	88, 55	sseqtrrid 3993	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
90	89, 58	sstrdi 3962	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
91	87, 90	sstrd 3960	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
92	91	unssad 4159	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
93		vpwex 5335	. . . . . . . . . 10 ⊢ 𝒫 𝑎 ∈ V
94		vuniex 7718	. . . . . . . . . 10 ⊢ ∪ 𝑎 ∈ V
95	93, 94	prss 4787	. . . . . . . . 9 ⊢ ((𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈) ↔ {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
96	92, 95	sylibr 234	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈))
97	96	simprd 495	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑎 ∈ 𝑈)
98	96	simpld 494	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝒫 𝑎 ∈ 𝑈)
99	1	eleq2i 2821	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran 𝐹)
100		fnunirn 7231	. . . . . . . . . . 11 ⊢ (𝐹 Fn ω → (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)))
101	6, 100	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
102	99, 101	bitri 275	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
103		ordom 7855	. . . . . . . . . . . . . . . . 17 ⊢ Ord ω
104		simplrl 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑚 ∈ ω)
105		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑛 ∈ ω)
106		ordunel 7805	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω)
107	103, 104, 105, 106	mp3an2i 1468	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝑚 ∪ 𝑛) ∈ ω)
108		ssun1 4144	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛)
109		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
110	109	sseq2d 3982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑚)))
111		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
112	111	sseq2d 3982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑖)))
113		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = suc 𝑖 → (𝐹‘𝑘) = (𝐹‘suc 𝑖))
114	113	sseq2d 3982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = suc 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
115		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → (𝐹‘𝑘) = (𝐹‘(𝑚 ∪ 𝑛)))
116	115	sseq2d 3982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
117		ssidd 3973	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘𝑚))
118		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖))
119		suceq 6403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
120	119	fveq2d 6865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
121	118, 120	sseq12d 3983	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)))
122		ssun1 4144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
123	122, 13	sstri 3959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
124	25, 54	mpan2 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
125	123, 124	sseqtrrid 3993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚))
126	121, 125	vtoclga 3546	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ω → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
127	126	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
128		sstr2 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → ((𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
129	127, 128	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
130	110, 112, 114, 116, 117, 129	findsg 7876	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚 ∪ 𝑛)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
131	108, 130	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
132	107, 104, 131	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
133		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘𝑚))
134	132, 133	sseldd 3950	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
135	82	mpteq2dv 5204	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
136	135	rneqd 5905	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
137	81, 136	uneq12d 4135	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})))
138	137	ssiun2s 5015	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
139	134, 138	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
140		ssun2 4145	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
141		fvex 6874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
142	141	uniex 7720	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
143	141, 142	unex 7723	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∈ V
144	141	mptex 7200	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
145	144	rnex 7889	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
146	20, 145	unex 7723	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
147	141, 146	iunex 7950	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
148	143, 147	unex 7723	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
149		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → 𝑤 = (𝐹‘(𝑚 ∪ 𝑛)))
150		unieq 4885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑤 = ∪ (𝐹‘(𝑚 ∪ 𝑛)))
151	149, 150	uneq12d 4135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))))
152		mpteq1 5199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
153	152	rneqd 5905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
154	153	uneq2d 4134	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
155	149, 154	iuneq12d 4988	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
156	151, 155	uneq12d 4135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
157	4, 45, 156	frsucmpt2 8411	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
158	107, 148, 157	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
159	140, 158	sseqtrrid 3993	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚 ∪ 𝑛)))
160		fvssunirn 6894	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ ran 𝐹
161	160, 1	sseqtrri 3999	. . . . . . . . . . . . . 14 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ 𝑈
162	159, 161	sstrdi 3962	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
163	139, 162	sstrd 3960	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
164	163	unssbd 4160	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
165		ssun2 4145	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛)
166		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑖 = (𝑚 ∪ 𝑛))
167	165, 166	sseqtrrid 3993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑛 ⊆ 𝑖)
168	167	biantrud 531	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖)))
169	168	bicomd 223	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) ↔ 𝑛 ∈ ω))
170		fveq2 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝐹‘𝑖) = (𝐹‘(𝑚 ∪ 𝑛)))
171	170	sseq2d 3982	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
172	169, 171	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) ↔ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))))
173		eleq1w 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
174	173	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
175		sseq1 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖))
176	174, 175	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖)))
177		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
178	177	sseq1d 3981	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
179	176, 178	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))))
180	110, 112, 114, 112, 117, 129	findsg 7876	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖))
181	179, 180	chvarvv 1989	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))
182	181	expl 457	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
183	172, 182	vtoclga 3546	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∪ 𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
184	107, 105, 183	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
185		simprr 772	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘𝑛))
186	184, 185	sseldd 3950	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
187		prex 5395	. . . . . . . . . . . 12 ⊢ {𝑎, 𝑏} ∈ V
188		eqid 2730	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})
189		preq2 4701	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
190	188, 189	elrnmpt1s 5926	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
191	186, 187, 190	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
192	164, 191	sseldd 3950	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
193	192	rexlimdvaa 3136	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛) → {𝑎, 𝑏} ∈ 𝑈))
194	102, 193	biimtrid 242	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝑏 ∈ 𝑈 → {𝑎, 𝑏} ∈ 𝑈))
195	194	ralrimiv 3125	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)
196	97, 98, 195	3jca 1128	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
197	196	rexlimdvaa 3136	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
198	9, 197	biimtrid 242	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
199	198	ralrimiv 3125	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
200		rdgfun 8387	. . . . . . . . 9 ⊢ Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o))
201		omex 9603	. . . . . . . . 9 ⊢ ω ∈ V
202		resfunexg 7192	. . . . . . . . 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 2825	. . . . . . 7 ⊢ 𝐹 ∈ V
205	204	rnex 7889	. . . . . 6 ⊢ ran 𝐹 ∈ V
206	205	uniex 7720	. . . . 5 ⊢ ∪ ran 𝐹 ∈ V
207	1, 206	eqeltri 2825	. . . 4 ⊢ 𝑈 ∈ V
208		iswun 10664	. . . 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 4159	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈)
212	210, 211	jca 511	1 ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 Vcvv 3450 ∪ cun 3915 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 {cpr 4594 ∪ cuni 4874 ∪ ciun 4958 ↦ cmpt 5191 Tr wtr 5217 ran crn 5642 ↾ cres 5643 Ord word 6334 Oncon0 6335 suc csuc 6337 Fun wfun 6508 Fn wfn 6509 ‘cfv 6514 ωcom 7845 reccrdg 8380 1_oc1o 8430 WUnicwun 10660

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-ov 7393 df-om 7846 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-wun 10662

This theorem is referenced by: wunex 10699 wuncval2 10707

W3C validator