r1val1

Description: The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of Enderton p. 202. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	r1val1	$⊢ A \in dom R_{1} \to R_{1} (A) = ⋃_{x \in A} 𝒫 R_{1} (x)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in dom R_{1} \land A = \emptyset) \to A = \emptyset$
2	1	fveq2d	$⊢ (A \in dom R_{1} \land A = \emptyset) \to R_{1} (A) = R_{1} (\emptyset)$
3		r10	$⊢ R_{1} (\emptyset) = \emptyset$
4	2 3	eqtrdi	$⊢ (A \in dom R_{1} \land A = \emptyset) \to R_{1} (A) = \emptyset$
5		0ss	$⊢ \emptyset \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
6	5	a1i	$⊢ (A \in dom R_{1} \land A = \emptyset) \to \emptyset \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
7	4 6	eqsstrd	$⊢ (A \in dom R_{1} \land A = \emptyset) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
8		nfv	$⊢ Ⅎ x A \in dom R_{1}$
9		nfcv	$⊢ \underline{Ⅎ} x R_{1} (A)$
10		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} 𝒫 R_{1} (x)$
11	9 10	nfss	$⊢ Ⅎ x R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
12		simpr	$⊢ (A \in dom R_{1} \land A = suc x) \to A = suc x$
13	12	fveq2d	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (A) = R_{1} (suc x)$
14		eleq1	$⊢ A = suc x \to (A \in dom R_{1} \leftrightarrow suc x \in dom R_{1})$
15	14	biimpac	$⊢ (A \in dom R_{1} \land A = suc x) \to suc x \in dom R_{1}$
16		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
17	16	simpri	$⊢ Lim dom R_{1}$
18		limsuc	$⊢ Lim dom R_{1} \to (x \in dom R_{1} \leftrightarrow suc x \in dom R_{1})$
19	17 18	ax-mp	$⊢ x \in dom R_{1} \leftrightarrow suc x \in dom R_{1}$
20	15 19	sylibr	$⊢ (A \in dom R_{1} \land A = suc x) \to x \in dom R_{1}$
21		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
22	20 21	syl	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
23	13 22	eqtrd	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (A) = 𝒫 R_{1} (x)$
24		vex	$⊢ x \in V$
25	24	sucid	$⊢ x \in suc x$
26	25 12	eleqtrrid	$⊢ (A \in dom R_{1} \land A = suc x) \to x \in A$
27		ssiun2	$⊢ x \in A \to 𝒫 R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
28	26 27	syl	$⊢ (A \in dom R_{1} \land A = suc x) \to 𝒫 R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
29	23 28	eqsstrd	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
30	29	ex	$⊢ A \in dom R_{1} \to (A = suc x \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x))$
31	30	a1d	$⊢ A \in dom R_{1} \to (x \in On \to (A = suc x \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)))$
32	8 11 31	rexlimd	$⊢ A \in dom R_{1} \to (\exists x \in On A = suc x \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x))$
33	32	imp	$⊢ (A \in dom R_{1} \land \exists x \in On A = suc x) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
34		r1limg	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
35		r1tr	$⊢ Tr R_{1} (x)$
36		dftr4	$⊢ Tr R_{1} (x) \leftrightarrow R_{1} (x) \subseteq 𝒫 R_{1} (x)$
37	35 36	mpbi	$⊢ R_{1} (x) \subseteq 𝒫 R_{1} (x)$
38	37	a1i	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (x) \subseteq 𝒫 R_{1} (x)$
39	38	ralrimivw	$⊢ (A \in dom R_{1} \land Lim A) \to \forall x \in A R_{1} (x) \subseteq 𝒫 R_{1} (x)$
40		ss2iun	$⊢ \forall x \in A R_{1} (x) \subseteq 𝒫 R_{1} (x) \to ⋃_{x \in A} R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
41	39 40	syl	$⊢ (A \in dom R_{1} \land Lim A) \to ⋃_{x \in A} R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
42	34 41	eqsstrd	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
43	42	adantrl	$⊢ (A \in dom R_{1} \land (A \in V \land Lim A)) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
44		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
45	17 44	ax-mp	$⊢ Ord dom R_{1}$
46		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
47	45 46	ax-mp	$⊢ dom R_{1} \subseteq On$
48	47	sseli	$⊢ A \in dom R_{1} \to A \in On$
49		onzsl	$⊢ A \in On \leftrightarrow (A = \emptyset \lor \exists x \in On A = suc x \lor (A \in V \land Lim A))$
50	48 49	sylib	$⊢ A \in dom R_{1} \to (A = \emptyset \lor \exists x \in On A = suc x \lor (A \in V \land Lim A))$
51	7 33 43 50	mpjao3dan	$⊢ A \in dom R_{1} \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
52		ordtr1	$⊢ Ord dom R_{1} \to ((x \in A \land A \in dom R_{1}) \to x \in dom R_{1})$
53	45 52	ax-mp	$⊢ (x \in A \land A \in dom R_{1}) \to x \in dom R_{1}$
54	53	ancoms	$⊢ (A \in dom R_{1} \land x \in A) \to x \in dom R_{1}$
55	54 21	syl	$⊢ (A \in dom R_{1} \land x \in A) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
56		simpr	$⊢ (A \in dom R_{1} \land x \in A) \to x \in A$
57		ordelord	$⊢ (Ord dom R_{1} \land A \in dom R_{1}) \to Ord A$
58	45 57	mpan	$⊢ A \in dom R_{1} \to Ord A$
59	58	adantr	$⊢ (A \in dom R_{1} \land x \in A) \to Ord A$
60		ordelsuc	$⊢ (x \in A \land Ord A) \to (x \in A \leftrightarrow suc x \subseteq A)$
61	56 59 60	syl2anc	$⊢ (A \in dom R_{1} \land x \in A) \to (x \in A \leftrightarrow suc x \subseteq A)$
62	56 61	mpbid	$⊢ (A \in dom R_{1} \land x \in A) \to suc x \subseteq A$
63	54 19	sylib	$⊢ (A \in dom R_{1} \land x \in A) \to suc x \in dom R_{1}$
64		simpl	$⊢ (A \in dom R_{1} \land x \in A) \to A \in dom R_{1}$
65		r1ord3g	$⊢ (suc x \in dom R_{1} \land A \in dom R_{1}) \to (suc x \subseteq A \to R_{1} (suc x) \subseteq R_{1} (A))$
66	63 64 65	syl2anc	$⊢ (A \in dom R_{1} \land x \in A) \to (suc x \subseteq A \to R_{1} (suc x) \subseteq R_{1} (A))$
67	62 66	mpd	$⊢ (A \in dom R_{1} \land x \in A) \to R_{1} (suc x) \subseteq R_{1} (A)$
68	55 67	eqsstrrd	$⊢ (A \in dom R_{1} \land x \in A) \to 𝒫 R_{1} (x) \subseteq R_{1} (A)$
69	68	ralrimiva	$⊢ A \in dom R_{1} \to \forall x \in A 𝒫 R_{1} (x) \subseteq R_{1} (A)$
70		iunss	$⊢ ⋃_{x \in A} 𝒫 R_{1} (x) \subseteq R_{1} (A) \leftrightarrow \forall x \in A 𝒫 R_{1} (x) \subseteq R_{1} (A)$
71	69 70	sylibr	$⊢ A \in dom R_{1} \to ⋃_{x \in A} 𝒫 R_{1} (x) \subseteq R_{1} (A)$
72	51 71	eqssd	$⊢ A \in dom R_{1} \to R_{1} (A) = ⋃_{x \in A} 𝒫 R_{1} (x)$

Metamath Proof Explorer

Theorem r1val1

Proof