wunex2

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

	Ref	Expression
Hypotheses	wunex2.f	$⊢ F = {rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω}$
	wunex2.u	$⊢ U = ⋃ ran F$
Assertion	wunex2	$⊢ A \in V \to (U \in WUni \land A \subseteq U)$

Proof

Step	Hyp	Ref	Expression
1		wunex2.f	$⊢ F = {rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω}$
2		wunex2.u	$⊢ U = ⋃ ran F$
3	2	eleq2i	$⊢ a \in U \leftrightarrow a \in ⋃ ran F$
4		frfnom	$⊢ ({rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω}) Fn ω$
5	1	fneq1i	$⊢ F Fn ω \leftrightarrow ({rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω}) Fn ω$
6	4 5	mpbir	$⊢ F Fn ω$
7		fnunirn	$⊢ F Fn ω \to (a \in ⋃ ran F \leftrightarrow \exists m \in ω a \in F (m))$
8	6 7	ax-mp	$⊢ a \in ⋃ ran F \leftrightarrow \exists m \in ω a \in F (m)$
9	3 8	bitri	$⊢ a \in U \leftrightarrow \exists m \in ω a \in F (m)$
10		elssuni	$⊢ a \in F (m) \to a \subseteq ⋃ F (m)$
11	10	ad2antll	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to a \subseteq ⋃ F (m)$
12		ssun2	$⊢ ⋃ F (m) \subseteq F (m) \cup ⋃ F (m)$
13		ssun1	$⊢ F (m) \cup ⋃ F (m) \subseteq (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
14	12 13	sstri	$⊢ ⋃ F (m) \subseteq (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
15	11 14	sstrdi	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to a \subseteq (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
16		simprl	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to m \in ω$
17		fvex	$⊢ F (m) \in V$
18	17	uniex	$⊢ ⋃ F (m) \in V$
19	17 18	unex	$⊢ F (m) \cup ⋃ F (m) \in V$
20		prex	$⊢ \{𝒫 u, ⋃ u\} \in V$
21	17	mptex	$⊢ (v \in F (m) ⟼ \{u, v\}) \in V$
22	21	rnex	$⊢ ran (v \in F (m) ⟼ \{u, v\}) \in V$
23	20 22	unex	$⊢ \{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}) \in V$
24	17 23	iunex	$⊢ ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})) \in V$
25	19 24	unex	$⊢ (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})) \in V$
26		id	$⊢ w = z \to w = z$
27		unieq	$⊢ w = z \to ⋃ w = ⋃ z$
28	26 27	uneq12d	$⊢ w = z \to w \cup ⋃ w = z \cup ⋃ z$
29		pweq	$⊢ u = x \to 𝒫 u = 𝒫 x$
30		unieq	$⊢ u = x \to ⋃ u = ⋃ x$
31	29 30	preq12d	$⊢ u = x \to \{𝒫 u, ⋃ u\} = \{𝒫 x, ⋃ x\}$
32		preq2	$⊢ v = y \to \{u, v\} = \{u, y\}$
33	32	cbvmptv	$⊢ (v \in w ⟼ \{u, v\}) = (y \in w ⟼ \{u, y\})$
34		preq1	$⊢ u = x \to \{u, y\} = \{x, y\}$
35	34	mpteq2dv	$⊢ u = x \to (y \in w ⟼ \{u, y\}) = (y \in w ⟼ \{x, y\})$
36	33 35	eqtrid	$⊢ u = x \to (v \in w ⟼ \{u, v\}) = (y \in w ⟼ \{x, y\})$
37	36	rneqd	$⊢ u = x \to ran (v \in w ⟼ \{u, v\}) = ran (y \in w ⟼ \{x, y\})$
38	31 37	uneq12d	$⊢ u = x \to \{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\}) = \{𝒫 x, ⋃ x\} \cup ran (y \in w ⟼ \{x, y\})$
39	38	cbviunv	$⊢ ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = ⋃_{x \in w} (\{𝒫 x, ⋃ x\} \cup ran (y \in w ⟼ \{x, y\}))$
40		mpteq1	$⊢ w = z \to (y \in w ⟼ \{x, y\}) = (y \in z ⟼ \{x, y\})$
41	40	rneqd	$⊢ w = z \to ran (y \in w ⟼ \{x, y\}) = ran (y \in z ⟼ \{x, y\})$
42	41	uneq2d	$⊢ w = z \to \{𝒫 x, ⋃ x\} \cup ran (y \in w ⟼ \{x, y\}) = \{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\})$
43	26 42	iuneq12d	$⊢ w = z \to ⋃_{x \in w} (\{𝒫 x, ⋃ x\} \cup ran (y \in w ⟼ \{x, y\})) = ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))$
44	39 43	eqtrid	$⊢ w = z \to ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))$
45	28 44	uneq12d	$⊢ w = z \to (w \cup ⋃ w) \cup ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))$
46		id	$⊢ w = F (m) \to w = F (m)$
47		unieq	$⊢ w = F (m) \to ⋃ w = ⋃ F (m)$
48	46 47	uneq12d	$⊢ w = F (m) \to w \cup ⋃ w = F (m) \cup ⋃ F (m)$
49		mpteq1	$⊢ w = F (m) \to (v \in w ⟼ \{u, v\}) = (v \in F (m) ⟼ \{u, v\})$
50	49	rneqd	$⊢ w = F (m) \to ran (v \in w ⟼ \{u, v\}) = ran (v \in F (m) ⟼ \{u, v\})$
51	50	uneq2d	$⊢ w = F (m) \to \{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\}) = \{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})$
52	46 51	iuneq12d	$⊢ w = F (m) \to ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
53	48 52	uneq12d	$⊢ w = F (m) \to (w \cup ⋃ w) \cup ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
54	1 45 53	frsucmpt2w	$⊢ (m \in ω \land (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})) \in V) \to F (suc m) = (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
55	16 25 54	sylancl	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to F (suc m) = (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
56	15 55	sseqtrrd	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to a \subseteq F (suc m)$
57		fvssunirn	$⊢ F (suc m) \subseteq ⋃ ran F$
58	57 2	sseqtrri	$⊢ F (suc m) \subseteq U$
59	56 58	sstrdi	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to a \subseteq U$
60	59	rexlimdvaa	$⊢ A \in V \to (\exists m \in ω a \in F (m) \to a \subseteq U)$
61	9 60	syl5bi	$⊢ A \in V \to (a \in U \to a \subseteq U)$
62	61	ralrimiv	$⊢ A \in V \to \forall a \in U a \subseteq U$
63		dftr3	$⊢ Tr U \leftrightarrow \forall a \in U a \subseteq U$
64	62 63	sylibr	$⊢ A \in V \to Tr U$
65		1on	$⊢ 1_{𝑜} \in On$
66		unexg	$⊢ (A \in V \land 1_{𝑜} \in On) \to A \cup 1_{𝑜} \in V$
67	65 66	mpan2	$⊢ A \in V \to A \cup 1_{𝑜} \in V$
68	1	fveq1i	$⊢ F (\emptyset) = ({rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω}) (\emptyset)$
69		fr0g	$⊢ A \cup 1_{𝑜} \in V \to ({rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω}) (\emptyset) = A \cup 1_{𝑜}$
70	68 69	eqtrid	$⊢ A \cup 1_{𝑜} \in V \to F (\emptyset) = A \cup 1_{𝑜}$
71	67 70	syl	$⊢ A \in V \to F (\emptyset) = A \cup 1_{𝑜}$
72		fvssunirn	$⊢ F (\emptyset) \subseteq ⋃ ran F$
73	72 2	sseqtrri	$⊢ F (\emptyset) \subseteq U$
74	71 73	eqsstrrdi	$⊢ A \in V \to A \cup 1_{𝑜} \subseteq U$
75	74	unssbd	$⊢ A \in V \to 1_{𝑜} \subseteq U$
76		1n0	$⊢ 1_{𝑜} \neq \emptyset$
77		ssn0	$⊢ (1_{𝑜} \subseteq U \land 1_{𝑜} \neq \emptyset) \to U \neq \emptyset$
78	75 76 77	sylancl	$⊢ A \in V \to U \neq \emptyset$
79		pweq	$⊢ u = a \to 𝒫 u = 𝒫 a$
80		unieq	$⊢ u = a \to ⋃ u = ⋃ a$
81	79 80	preq12d	$⊢ u = a \to \{𝒫 u, ⋃ u\} = \{𝒫 a, ⋃ a\}$
82		preq1	$⊢ u = a \to \{u, v\} = \{a, v\}$
83	82	mpteq2dv	$⊢ u = a \to (v \in F (m) ⟼ \{u, v\}) = (v \in F (m) ⟼ \{a, v\})$
84	83	rneqd	$⊢ u = a \to ran (v \in F (m) ⟼ \{u, v\}) = ran (v \in F (m) ⟼ \{a, v\})$
85	81 84	uneq12d	$⊢ u = a \to \{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}) = \{𝒫 a, ⋃ a\} \cup ran (v \in F (m) ⟼ \{a, v\})$
86	85	ssiun2s	$⊢ a \in F (m) \to \{𝒫 a, ⋃ a\} \cup ran (v \in F (m) ⟼ \{a, v\}) \subseteq ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
87	86	ad2antll	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to \{𝒫 a, ⋃ a\} \cup ran (v \in F (m) ⟼ \{a, v\}) \subseteq ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
88		ssun2	$⊢ ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})) \subseteq (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
89	88 55	sseqtrrid	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})) \subseteq F (suc m)$
90	89 58	sstrdi	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\})) \subseteq U$
91	87 90	sstrd	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to \{𝒫 a, ⋃ a\} \cup ran (v \in F (m) ⟼ \{a, v\}) \subseteq U$
92	91	unssad	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to \{𝒫 a, ⋃ a\} \subseteq U$
93		vpwex	$⊢ 𝒫 a \in V$
94		vuniex	$⊢ ⋃ a \in V$
95	93 94	prss	$⊢ (𝒫 a \in U \land ⋃ a \in U) \leftrightarrow \{𝒫 a, ⋃ a\} \subseteq U$
96	92 95	sylibr	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to (𝒫 a \in U \land ⋃ a \in U)$
97	96	simprd	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to ⋃ a \in U$
98	96	simpld	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to 𝒫 a \in U$
99	2	eleq2i	$⊢ b \in U \leftrightarrow b \in ⋃ ran F$
100		fnunirn	$⊢ F Fn ω \to (b \in ⋃ ran F \leftrightarrow \exists n \in ω b \in F (n))$
101	6 100	ax-mp	$⊢ b \in ⋃ ran F \leftrightarrow \exists n \in ω b \in F (n)$
102	99 101	bitri	$⊢ b \in U \leftrightarrow \exists n \in ω b \in F (n)$
103		ordom	$⊢ Ord ω$
104		simplrl	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to m \in ω$
105		simprl	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to n \in ω$
106		ordunel	$⊢ (Ord ω \land m \in ω \land n \in ω) \to m \cup n \in ω$
107	103 104 105 106	mp3an2i	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to m \cup n \in ω$
108		ssun1	$⊢ m \subseteq m \cup n$
109		fveq2	$⊢ k = m \to F (k) = F (m)$
110	109	sseq2d	$⊢ k = m \to (F (m) \subseteq F (k) \leftrightarrow F (m) \subseteq F (m))$
111		fveq2	$⊢ k = i \to F (k) = F (i)$
112	111	sseq2d	$⊢ k = i \to (F (m) \subseteq F (k) \leftrightarrow F (m) \subseteq F (i))$
113		fveq2	$⊢ k = suc i \to F (k) = F (suc i)$
114	113	sseq2d	$⊢ k = suc i \to (F (m) \subseteq F (k) \leftrightarrow F (m) \subseteq F (suc i))$
115		fveq2	$⊢ k = m \cup n \to F (k) = F (m \cup n)$
116	115	sseq2d	$⊢ k = m \cup n \to (F (m) \subseteq F (k) \leftrightarrow F (m) \subseteq F (m \cup n))$
117		ssidd	$⊢ m \in ω \to F (m) \subseteq F (m)$
118		fveq2	$⊢ m = i \to F (m) = F (i)$
119		suceq	$⊢ m = i \to suc m = suc i$
120	119	fveq2d	$⊢ m = i \to F (suc m) = F (suc i)$
121	118 120	sseq12d	$⊢ m = i \to (F (m) \subseteq F (suc m) \leftrightarrow F (i) \subseteq F (suc i))$
122		ssun1	$⊢ F (m) \subseteq F (m) \cup ⋃ F (m)$
123	122 13	sstri	$⊢ F (m) \subseteq (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
124	25 54	mpan2	$⊢ m \in ω \to F (suc m) = (F (m) \cup ⋃ F (m)) \cup ⋃_{u \in F (m)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m) ⟼ \{u, v\}))$
125	123 124	sseqtrrid	$⊢ m \in ω \to F (m) \subseteq F (suc m)$
126	121 125	vtoclga	$⊢ i \in ω \to F (i) \subseteq F (suc i)$
127	126	ad2antrr	$⊢ ((i \in ω \land m \in ω) \land m \subseteq i) \to F (i) \subseteq F (suc i)$
128		sstr2	$⊢ F (m) \subseteq F (i) \to (F (i) \subseteq F (suc i) \to F (m) \subseteq F (suc i))$
129	127 128	syl5com	$⊢ ((i \in ω \land m \in ω) \land m \subseteq i) \to (F (m) \subseteq F (i) \to F (m) \subseteq F (suc i))$
130	110 112 114 116 117 129	findsg	$⊢ ((m \cup n \in ω \land m \in ω) \land m \subseteq m \cup n) \to F (m) \subseteq F (m \cup n)$
131	108 130	mpan2	$⊢ (m \cup n \in ω \land m \in ω) \to F (m) \subseteq F (m \cup n)$
132	107 104 131	syl2anc	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to F (m) \subseteq F (m \cup n)$
133		simplrr	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to a \in F (m)$
134	132 133	sseldd	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to a \in F (m \cup n)$
135	82	mpteq2dv	$⊢ u = a \to (v \in F (m \cup n) ⟼ \{u, v\}) = (v \in F (m \cup n) ⟼ \{a, v\})$
136	135	rneqd	$⊢ u = a \to ran (v \in F (m \cup n) ⟼ \{u, v\}) = ran (v \in F (m \cup n) ⟼ \{a, v\})$
137	81 136	uneq12d	$⊢ u = a \to \{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}) = \{𝒫 a, ⋃ a\} \cup ran (v \in F (m \cup n) ⟼ \{a, v\})$
138	137	ssiun2s	$⊢ a \in F (m \cup n) \to \{𝒫 a, ⋃ a\} \cup ran (v \in F (m \cup n) ⟼ \{a, v\}) \subseteq ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
139	134 138	syl	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to \{𝒫 a, ⋃ a\} \cup ran (v \in F (m \cup n) ⟼ \{a, v\}) \subseteq ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
140		ssun2	$⊢ ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})) \subseteq (F (m \cup n) \cup ⋃ F (m \cup n)) \cup ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
141		fvex	$⊢ F (m \cup n) \in V$
142	141	uniex	$⊢ ⋃ F (m \cup n) \in V$
143	141 142	unex	$⊢ F (m \cup n) \cup ⋃ F (m \cup n) \in V$
144	141	mptex	$⊢ (v \in F (m \cup n) ⟼ \{u, v\}) \in V$
145	144	rnex	$⊢ ran (v \in F (m \cup n) ⟼ \{u, v\}) \in V$
146	20 145	unex	$⊢ \{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}) \in V$
147	141 146	iunex	$⊢ ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})) \in V$
148	143 147	unex	$⊢ (F (m \cup n) \cup ⋃ F (m \cup n)) \cup ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})) \in V$
149		id	$⊢ w = F (m \cup n) \to w = F (m \cup n)$
150		unieq	$⊢ w = F (m \cup n) \to ⋃ w = ⋃ F (m \cup n)$
151	149 150	uneq12d	$⊢ w = F (m \cup n) \to w \cup ⋃ w = F (m \cup n) \cup ⋃ F (m \cup n)$
152		mpteq1	$⊢ w = F (m \cup n) \to (v \in w ⟼ \{u, v\}) = (v \in F (m \cup n) ⟼ \{u, v\})$
153	152	rneqd	$⊢ w = F (m \cup n) \to ran (v \in w ⟼ \{u, v\}) = ran (v \in F (m \cup n) ⟼ \{u, v\})$
154	153	uneq2d	$⊢ w = F (m \cup n) \to \{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\}) = \{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})$
155	149 154	iuneq12d	$⊢ w = F (m \cup n) \to ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
156	151 155	uneq12d	$⊢ w = F (m \cup n) \to (w \cup ⋃ w) \cup ⋃_{u \in w} (\{𝒫 u, ⋃ u\} \cup ran (v \in w ⟼ \{u, v\})) = (F (m \cup n) \cup ⋃ F (m \cup n)) \cup ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
157	1 45 156	frsucmpt2w	$⊢ (m \cup n \in ω \land (F (m \cup n) \cup ⋃ F (m \cup n)) \cup ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})) \in V) \to F (suc (m \cup n)) = (F (m \cup n) \cup ⋃ F (m \cup n)) \cup ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
158	107 148 157	sylancl	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to F (suc (m \cup n)) = (F (m \cup n) \cup ⋃ F (m \cup n)) \cup ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\}))$
159	140 158	sseqtrrid	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})) \subseteq F (suc (m \cup n))$
160		fvssunirn	$⊢ F (suc (m \cup n)) \subseteq ⋃ ran F$
161	160 2	sseqtrri	$⊢ F (suc (m \cup n)) \subseteq U$
162	159 161	sstrdi	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to ⋃_{u \in F (m \cup n)} (\{𝒫 u, ⋃ u\} \cup ran (v \in F (m \cup n) ⟼ \{u, v\})) \subseteq U$
163	139 162	sstrd	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to \{𝒫 a, ⋃ a\} \cup ran (v \in F (m \cup n) ⟼ \{a, v\}) \subseteq U$
164	163	unssbd	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to ran (v \in F (m \cup n) ⟼ \{a, v\}) \subseteq U$
165		ssun2	$⊢ n \subseteq m \cup n$
166		id	$⊢ i = m \cup n \to i = m \cup n$
167	165 166	sseqtrrid	$⊢ i = m \cup n \to n \subseteq i$
168	167	biantrud	$⊢ i = m \cup n \to (n \in ω \leftrightarrow (n \in ω \land n \subseteq i))$
169	168	bicomd	$⊢ i = m \cup n \to ((n \in ω \land n \subseteq i) \leftrightarrow n \in ω)$
170		fveq2	$⊢ i = m \cup n \to F (i) = F (m \cup n)$
171	170	sseq2d	$⊢ i = m \cup n \to (F (n) \subseteq F (i) \leftrightarrow F (n) \subseteq F (m \cup n))$
172	169 171	imbi12d	$⊢ i = m \cup n \to (((n \in ω \land n \subseteq i) \to F (n) \subseteq F (i)) \leftrightarrow (n \in ω \to F (n) \subseteq F (m \cup n)))$
173		eleq1w	$⊢ m = n \to (m \in ω \leftrightarrow n \in ω)$
174	173	anbi2d	$⊢ m = n \to ((i \in ω \land m \in ω) \leftrightarrow (i \in ω \land n \in ω))$
175		sseq1	$⊢ m = n \to (m \subseteq i \leftrightarrow n \subseteq i)$
176	174 175	anbi12d	$⊢ m = n \to (((i \in ω \land m \in ω) \land m \subseteq i) \leftrightarrow ((i \in ω \land n \in ω) \land n \subseteq i))$
177		fveq2	$⊢ m = n \to F (m) = F (n)$
178	177	sseq1d	$⊢ m = n \to (F (m) \subseteq F (i) \leftrightarrow F (n) \subseteq F (i))$
179	176 178	imbi12d	$⊢ m = n \to ((((i \in ω \land m \in ω) \land m \subseteq i) \to F (m) \subseteq F (i)) \leftrightarrow (((i \in ω \land n \in ω) \land n \subseteq i) \to F (n) \subseteq F (i)))$
180	110 112 114 112 117 129	findsg	$⊢ ((i \in ω \land m \in ω) \land m \subseteq i) \to F (m) \subseteq F (i)$
181	179 180	chvarvv	$⊢ ((i \in ω \land n \in ω) \land n \subseteq i) \to F (n) \subseteq F (i)$
182	181	expl	$⊢ i \in ω \to ((n \in ω \land n \subseteq i) \to F (n) \subseteq F (i))$
183	172 182	vtoclga	$⊢ m \cup n \in ω \to (n \in ω \to F (n) \subseteq F (m \cup n))$
184	107 105 183	sylc	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to F (n) \subseteq F (m \cup n)$
185		simprr	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to b \in F (n)$
186	184 185	sseldd	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to b \in F (m \cup n)$
187		prex	$⊢ \{a, b\} \in V$
188		eqid	$⊢ (v \in F (m \cup n) ⟼ \{a, v\}) = (v \in F (m \cup n) ⟼ \{a, v\})$
189		preq2	$⊢ v = b \to \{a, v\} = \{a, b\}$
190	188 189	elrnmpt1s	$⊢ (b \in F (m \cup n) \land \{a, b\} \in V) \to \{a, b\} \in ran (v \in F (m \cup n) ⟼ \{a, v\})$
191	186 187 190	sylancl	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to \{a, b\} \in ran (v \in F (m \cup n) ⟼ \{a, v\})$
192	164 191	sseldd	$⊢ ((A \in V \land (m \in ω \land a \in F (m))) \land (n \in ω \land b \in F (n))) \to \{a, b\} \in U$
193	192	rexlimdvaa	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to (\exists n \in ω b \in F (n) \to \{a, b\} \in U)$
194	102 193	syl5bi	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to (b \in U \to \{a, b\} \in U)$
195	194	ralrimiv	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to \forall b \in U \{a, b\} \in U$
196	97 98 195	3jca	$⊢ (A \in V \land (m \in ω \land a \in F (m))) \to (⋃ a \in U \land 𝒫 a \in U \land \forall b \in U \{a, b\} \in U)$
197	196	rexlimdvaa	$⊢ A \in V \to (\exists m \in ω a \in F (m) \to (⋃ a \in U \land 𝒫 a \in U \land \forall b \in U \{a, b\} \in U))$
198	9 197	syl5bi	$⊢ A \in V \to (a \in U \to (⋃ a \in U \land 𝒫 a \in U \land \forall b \in U \{a, b\} \in U))$
199	198	ralrimiv	$⊢ A \in V \to \forall a \in U (⋃ a \in U \land 𝒫 a \in U \land \forall b \in U \{a, b\} \in U)$
200		rdgfun	$⊢ Fun rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜})$
201		omex	$⊢ ω \in V$
202		resfunexg	$⊢ (Fun rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) \land ω \in V) \to {rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω} \in V$
203	200 201 202	mp2an	$⊢ {rec ((z \in V ⟼ (z \cup ⋃ z) \cup ⋃_{x \in z} (\{𝒫 x, ⋃ x\} \cup ran (y \in z ⟼ \{x, y\}))), A \cup 1_{𝑜}) ↾}_{ω} \in V$
204	1 203	eqeltri	$⊢ F \in V$
205	204	rnex	$⊢ ran F \in V$
206	205	uniex	$⊢ ⋃ ran F \in V$
207	2 206	eqeltri	$⊢ U \in V$
208		iswun	$⊢ U \in V \to (U \in WUni \leftrightarrow (Tr U \land U \neq \emptyset \land \forall a \in U (⋃ a \in U \land 𝒫 a \in U \land \forall b \in U \{a, b\} \in U)))$
209	207 208	ax-mp	$⊢ U \in WUni \leftrightarrow (Tr U \land U \neq \emptyset \land \forall a \in U (⋃ a \in U \land 𝒫 a \in U \land \forall b \in U \{a, b\} \in U))$
210	64 78 199 209	syl3anbrc	$⊢ A \in V \to U \in WUni$
211	74	unssad	$⊢ A \in V \to A \subseteq U$
212	210 211	jca	$⊢ A \in V \to (U \in WUni \land A \subseteq U)$

Metamath Proof Explorer

Theorem wunex2

Proof