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		r1dmlim	$⊢ Lim dom R_{1}$
17		limsuc	$⊢ Lim dom R_{1} \to (x \in dom R_{1} \leftrightarrow suc x \in dom R_{1})$
18	16 17	ax-mp	$⊢ x \in dom R_{1} \leftrightarrow suc x \in dom R_{1}$
19	15 18	sylibr	$⊢ (A \in dom R_{1} \land A = suc x) \to x \in dom R_{1}$
20		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
21	19 20	syl	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
22	13 21	eqtrd	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (A) = 𝒫 R_{1} (x)$
23		vex	$⊢ x \in V$
24	23	sucid	$⊢ x \in suc x$
25	24 12	eleqtrrid	$⊢ (A \in dom R_{1} \land A = suc x) \to x \in A$
26		ssiun2	$⊢ x \in A \to 𝒫 R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
27	25 26	syl	$⊢ (A \in dom R_{1} \land A = suc x) \to 𝒫 R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
28	22 27	eqsstrd	$⊢ (A \in dom R_{1} \land A = suc x) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
29	28	ex	$⊢ A \in dom R_{1} \to (A = suc x \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x))$
30	29	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)))$
31	8 11 30	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))$
32	31	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)$
33		r1limg	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
34		r1tr	$⊢ Tr R_{1} (x)$
35		dftr4	$⊢ Tr R_{1} (x) \leftrightarrow R_{1} (x) \subseteq 𝒫 R_{1} (x)$
36	34 35	mpbi	$⊢ R_{1} (x) \subseteq 𝒫 R_{1} (x)$
37	36	a1i	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (x) \subseteq 𝒫 R_{1} (x)$
38	37	ralrimivw	$⊢ (A \in dom R_{1} \land Lim A) \to \forall x \in A R_{1} (x) \subseteq 𝒫 R_{1} (x)$
39		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)$
40	38 39	syl	$⊢ (A \in dom R_{1} \land Lim A) \to ⋃_{x \in A} R_{1} (x) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
41	33 40	eqsstrd	$⊢ (A \in dom R_{1} \land Lim A) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
42	41	adantrl	$⊢ (A \in dom R_{1} \land (A \in V \land Lim A)) \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
43		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
44	16 43	ax-mp	$⊢ Ord dom R_{1}$
45		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
46	44 45	ax-mp	$⊢ dom R_{1} \subseteq On$
47	46	sseli	$⊢ A \in dom R_{1} \to A \in On$
48		onzsl	$⊢ A \in On \leftrightarrow (A = \emptyset \lor \exists x \in On A = suc x \lor (A \in V \land Lim A))$
49	47 48	sylib	$⊢ A \in dom R_{1} \to (A = \emptyset \lor \exists x \in On A = suc x \lor (A \in V \land Lim A))$
50	7 32 42 49	mpjao3dan	$⊢ A \in dom R_{1} \to R_{1} (A) \subseteq ⋃_{x \in A} 𝒫 R_{1} (x)$
51		ordtr1	$⊢ Ord dom R_{1} \to ((x \in A \land A \in dom R_{1}) \to x \in dom R_{1})$
52	44 51	ax-mp	$⊢ (x \in A \land A \in dom R_{1}) \to x \in dom R_{1}$
53	52	ancoms	$⊢ (A \in dom R_{1} \land x \in A) \to x \in dom R_{1}$
54	53 20	syl	$⊢ (A \in dom R_{1} \land x \in A) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
55		simpr	$⊢ (A \in dom R_{1} \land x \in A) \to x \in A$
56		ordelord	$⊢ (Ord dom R_{1} \land A \in dom R_{1}) \to Ord A$
57	44 56	mpan	$⊢ A \in dom R_{1} \to Ord A$
58	57	adantr	$⊢ (A \in dom R_{1} \land x \in A) \to Ord A$
59		ordelsuc	$⊢ (x \in A \land Ord A) \to (x \in A \leftrightarrow suc x \subseteq A)$
60	55 58 59	syl2anc	$⊢ (A \in dom R_{1} \land x \in A) \to (x \in A \leftrightarrow suc x \subseteq A)$
61	55 60	mpbid	$⊢ (A \in dom R_{1} \land x \in A) \to suc x \subseteq A$
62	53 18	sylib	$⊢ (A \in dom R_{1} \land x \in A) \to suc x \in dom R_{1}$
63		simpl	$⊢ (A \in dom R_{1} \land x \in A) \to A \in dom R_{1}$
64		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))$
65	62 63 64	syl2anc	$⊢ (A \in dom R_{1} \land x \in A) \to (suc x \subseteq A \to R_{1} (suc x) \subseteq R_{1} (A))$
66	61 65	mpd	$⊢ (A \in dom R_{1} \land x \in A) \to R_{1} (suc x) \subseteq R_{1} (A)$
67	54 66	eqsstrrd	$⊢ (A \in dom R_{1} \land x \in A) \to 𝒫 R_{1} (x) \subseteq R_{1} (A)$
68	67	ralrimiva	$⊢ A \in dom R_{1} \to \forall x \in A 𝒫 R_{1} (x) \subseteq R_{1} (A)$
69		iunss	$⊢ ⋃_{x \in A} 𝒫 R_{1} (x) \subseteq R_{1} (A) \leftrightarrow \forall x \in A 𝒫 R_{1} (x) \subseteq R_{1} (A)$
70	68 69	sylibr	$⊢ A \in dom R_{1} \to ⋃_{x \in A} 𝒫 R_{1} (x) \subseteq R_{1} (A)$
71	50 70	eqssd	$⊢ A \in dom R_{1} \to R_{1} (A) = ⋃_{x \in A} 𝒫 R_{1} (x)$

Metamath Proof Explorer

Theorem r1val1

Proof