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 10722

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 2861	. . . . . . 7 ⊢ (𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran 𝐹)
3		frfnom 8421	. . . . . . . . 9 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω
4		wunex2.f	. . . . . . . . . 10 ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)
5	4	fneq1i 6633	. . . . . . . . 9 ⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) Fn ω)
6	3, 5	mpbir 234	. . . . . . . 8 ⊢ 𝐹 Fn ω
7		fnunirn 7252	. . . . . . . 8 ⊢ (𝐹 Fn ω → (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
9	2, 8	bitri 278	. . . . . 6 ⊢ (𝑎 ∈ 𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))
10		elssuni 4908	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
11	10	ad2antll 741	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ ∪ (𝐹‘𝑚))
12		ssun2 4140	. . . . . . . . . . 11 ⊢ ∪ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
13		ssun1 4139	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
14	12, 13	sstri 3954	. . . . . . . . . 10 ⊢ ∪ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
15	11, 14	sstrdi 3957	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
16		simprl 782	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑚 ∈ ω)
17		fvex 6895	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑚) ∈ V
18	17	uniex 7739	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑚) ∈ V
19	17, 18	unex 7742	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∈ V
20		prex 5410	. . . . . . . . . . . . 13 ⊢ {𝒫 𝑢, ∪ 𝑢} ∈ V
21	17	mptex 7222	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
22	21	rnex 7906	. . . . . . . . . . . . 13 ⊢ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V
23	20, 22	unex 7742	. . . . . . . . . . . 12 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
24	17, 23	iunex 7964	. . . . . . . . . . 11 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V
25	19, 24	unex 7742	. . . . . . . . . 10 ⊢ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26		id 23	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
27		unieq 4887	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧)
28	26, 27	uneq12d 4131	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧))
29		pweq 4581	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30		unieq 4887	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥)
31	29, 30	preq12d 4712	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪ 𝑥})
32		preq2 4705	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
33	32	cbvmptv 5219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦})
34		preq1 4704	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
35	34	mpteq2dv 5209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
36	33, 35	eqtrid 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
37	36	rneqd 5929	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
38	31, 37	uneq12d 4131	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})))
39	38	cbviunv 5007	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))
40		mpteq1 5204	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
41	40	rneqd 5929	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))
42	41	uneq2d 4130	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
43	26, 42	iuneq12d 4990	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
44	39, 43	eqtrid 2816	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))
45	28, 44	uneq12d 4131	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))))
46		id 23	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → 𝑤 = (𝐹‘𝑚))
47		unieq 4887	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑤 = ∪ (𝐹‘𝑚))
48	46, 47	uneq12d 4131	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)))
49		mpteq1 5204	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐹‘𝑚) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
50	49	rneqd 5929	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐹‘𝑚) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))
51	50	uneq2d 4130	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑚) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
52	46, 51	iuneq12d 4990	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
53	48, 52	uneq12d 4131	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑚) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
54	4, 45, 53	frsucmpt2 8426	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
55	16, 25, 54	sylancl 597	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
56	15, 55	sseqtrrd 3982	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57		fvssunirn 6913	. . . . . . . . 9 ⊢ (𝐹‘suc 𝑚) ⊆ ∪ ran 𝐹
58	57, 1	sseqtrri 3994	. . . . . . . 8 ⊢ (𝐹‘suc 𝑚) ⊆ 𝑈
59	56, 58	sstrdi 3957	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ 𝑈)
60	59	rexlimdvaa 3173	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ 𝑈))
61	9, 60	biimtrid 245	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈))
62	61	ralrimiv 3162	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
63		dftr3 5227	. . . 4 ⊢ (Tr 𝑈 ↔ ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈)
64	62, 63	sylibr 237	. . 3 ⊢ (𝐴 ∈ 𝑉 → Tr 𝑈)
65		1on 8465	. . . . . . . 8 ⊢ 1_o ∈ On
66		unexg 7741	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 1_o ∈ On) → (𝐴 ∪ 1_o) ∈ V)
67	65, 66	mpan2 703	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ∈ V)
68	4	fveq1i 6883	. . . . . . . 8 ⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅)
69		fr0g 8422	. . . . . . . 8 ⊢ ((𝐴 ∪ 1_o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω)‘∅) = (𝐴 ∪ 1_o))
70	68, 69	eqtrid 2816	. . . . . . 7 ⊢ ((𝐴 ∪ 1_o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1_o))
71	67, 70	syl 18	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1_o))
72		fvssunirn 6913	. . . . . . 7 ⊢ (𝐹‘∅) ⊆ ∪ ran 𝐹
73	72, 1	sseqtrri 3994	. . . . . 6 ⊢ (𝐹‘∅) ⊆ 𝑈
74	71, 73	eqsstrrdi 3990	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1_o) ⊆ 𝑈)
75	74	unssbd 4155	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 1_o ⊆ 𝑈)
76		1n0 8471	. . . 4 ⊢ 1_o ≠ ∅
77		ssn0 4368	. . . 4 ⊢ ((1_o ⊆ 𝑈 ∧ 1_o ≠ ∅) → 𝑈 ≠ ∅)
78	75, 76, 77	sylancl 597	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ≠ ∅)
79		pweq 4581	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80		unieq 4887	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
81	79, 80	preq12d 4712	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑎, ∪ 𝑎})
82		preq1 4704	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
83	82	mpteq2dv 5209	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
84	83	rneqd 5929	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))
85	81, 84	uneq12d 4131	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})))
86	85	ssiun2s 5017	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐹‘𝑚) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
87	86	ad2antll 741	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
88		ssun2 4140	. . . . . . . . . . . . 13 ⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
89	88, 55	sseqtrrid 3988	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
90	89, 58	sstrdi 3957	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
91	87, 90	sstrd 3955	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
92	91	unssad 4154	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
93		vpwex 5349	. . . . . . . . . 10 ⊢ 𝒫 𝑎 ∈ V
94		vuniex 7737	. . . . . . . . . 10 ⊢ ∪ 𝑎 ∈ V
95	93, 94	prss 4790	. . . . . . . . 9 ⊢ ((𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈) ↔ {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈)
96	92, 95	sylibr 237	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈))
97	96	simprd 500	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑎 ∈ 𝑈)
98	96	simpld 499	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝒫 𝑎 ∈ 𝑈)
99	1	eleq2i 2861	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran 𝐹)
100		fnunirn 7252	. . . . . . . . . . 11 ⊢ (𝐹 Fn ω → (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)))
101	6, 100	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
102	99, 101	bitri 278	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))
103		ordom 7871	. . . . . . . . . . . . . . . . 17 ⊢ Ord ω
104		simplrl 788	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑚 ∈ ω)
105		simprl 782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑛 ∈ ω)
106		ordunel 7822	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω)
107	103, 104, 105, 106	mp3an2i 1492	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝑚 ∪ 𝑛) ∈ ω)
108		ssun1 4139	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛)
109		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
110	109	sseq2d 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑚)))
111		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
112	111	sseq2d 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑖)))
113		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = suc 𝑖 → (𝐹‘𝑘) = (𝐹‘suc 𝑖))
114	113	sseq2d 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = suc 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
115		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → (𝐹‘𝑘) = (𝐹‘(𝑚 ∪ 𝑛)))
116	115	sseq2d 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
117		ssidd 3968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘𝑚))
118		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖))
119		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
120	119	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
121	118, 120	sseq12d 3978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)))
122		ssun1 4139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))
123	122, 13	sstri 3954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))
124	25, 54	mpan2 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))))
125	123, 124	sseqtrrid 3988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚))
126	121, 125	vtoclga 3550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ω → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
127	126	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))
128		sstr2 3952	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → ((𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
129	127, 128	syl5com 32	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖)))
130	110, 112, 114, 116, 117, 129	findsg 7893	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚 ∪ 𝑛)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
131	108, 130	mpan2 703	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
132	107, 104, 131	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
133		simplrr 789	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘𝑚))
134	132, 133	sseldd 3946	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
135	82	mpteq2dv 5209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
136	135	rneqd 5929	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
137	81, 136	uneq12d 4131	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})))
138	137	ssiun2s 5017	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
139	134, 138	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
140		ssun2 4140	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
141		fvex 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
142	141	uniex 7739	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V
143	141, 142	unex 7742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∈ V
144	141	mptex 7222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
145	144	rnex 7906	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V
146	20, 145	unex 7742	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
147	141, 146	iunex 7964	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V
148	143, 147	unex 7742	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
149		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → 𝑤 = (𝐹‘(𝑚 ∪ 𝑛)))
150		unieq 4887	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑤 = ∪ (𝐹‘(𝑚 ∪ 𝑛)))
151	149, 150	uneq12d 4131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))))
152		mpteq1 5204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
153	152	rneqd 5929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))
154	153	uneq2d 4130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
155	149, 154	iuneq12d 4990	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))
156	151, 155	uneq12d 4131	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
157	4, 45, 156	frsucmpt2 8426	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
158	107, 148, 157	sylancl 597	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))))
159	140, 158	sseqtrrid 3988	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚 ∪ 𝑛)))
160		fvssunirn 6913	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ ran 𝐹
161	160, 1	sseqtrri 3994	. . . . . . . . . . . . . 14 ⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ 𝑈
162	159, 161	sstrdi 3957	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
163	139, 162	sstrd 3955	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
164	163	unssbd 4155	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
165		ssun2 4140	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛)
166		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑖 = (𝑚 ∪ 𝑛))
167	165, 166	sseqtrrid 3988	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑛 ⊆ 𝑖)
168	167	biantrud 540	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖)))
169	168	bicomd 226	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) ↔ 𝑛 ∈ ω))
170		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝐹‘𝑖) = (𝐹‘(𝑚 ∪ 𝑛)))
171	170	sseq2d 3977	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
172	169, 171	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑚 ∪ 𝑛) → (((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) ↔ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))))
173		eleq1w 2852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
174	173	anbi2d 641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
175		sseq1 3970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖))
176	174, 175	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖)))
177		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
178	177	sseq1d 3976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
179	176, 178	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))))
180	110, 112, 114, 112, 117, 129	findsg 7893	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖))
181	179, 180	chvarvv 2016	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))
182	181	expl 462	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))
183	172, 182	vtoclga 3550	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∪ 𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))
184	107, 105, 183	sylc 66	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))
185		simprr 784	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘𝑛))
186	184, 185	sseldd 3946	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)))
187		prex 5410	. . . . . . . . . . . 12 ⊢ {𝑎, 𝑏} ∈ V
188		eqid 2769	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})
189		preq2 4705	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
190	188, 189	elrnmpt1s 5950	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
191	186, 187, 190	sylancl 597	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))
192	164, 191	sseldd 3946	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
193	192	rexlimdvaa 3173	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛) → {𝑎, 𝑏} ∈ 𝑈))
194	102, 193	biimtrid 245	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝑏 ∈ 𝑈 → {𝑎, 𝑏} ∈ 𝑈))
195	194	ralrimiv 3162	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)
196	97, 98, 195	3jca 1144	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
197	196	rexlimdvaa 3173	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
198	9, 197	biimtrid 245	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
199	198	ralrimiv 3162	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))
200		rdgfun 8402	. . . . . . . . 9 ⊢ Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o))
201		omex 9611	. . . . . . . . 9 ⊢ ω ∈ V
202		resfunexg 7214	. . . . . . . . 9 ⊢ ((Fun rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) ∈ V)
203	200, 201, 202	mp2an 704	. . . . . . . 8 ⊢ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1_o)) ↾ ω) ∈ V
204	4, 203	eqeltri 2865	. . . . . . 7 ⊢ 𝐹 ∈ V
205	204	rnex 7906	. . . . . 6 ⊢ ran 𝐹 ∈ V
206	205	uniex 7739	. . . . 5 ⊢ ∪ ran 𝐹 ∈ V
207	1, 206	eqeltri 2865	. . . 4 ⊢ 𝑈 ∈ V
208		iswun 10688	. . . 4 ⊢ (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))))
209	207, 208	ax-mp 5	. . 3 ⊢ (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))
210	64, 78, 199, 209	syl3anbrc 1360	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝑈 ∈ WUni)
211	74	unssad 4154	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈)
212	210, 211	jca 520	1 ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ∪ cun 3911 ⊆ wss 3913 ∅c0 4294 𝒫 cpw 4567 {cpr 4596 ∪ cuni 4876 ∪ ciun 4960 ↦ cmpt 5196 Tr wtr 5222 ran crn 5663 ↾ cres 5664 Ord word 6360 Oncon0 6361 suc csuc 6363 Fun wfun 6531 Fn wfn 6532 ‘cfv 6537 ωcom 7861 reccrdg 8395 1_oc1o 8445 WUnicwun 10684

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9609

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7414 df-om 7862 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-wun 10686

This theorem is referenced by: wunex 10723 wuncval2 10731

W3C validator