r1ordg

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 8-Sep-2003)

		Ref	Expression
	Assertion	r1ordg	$⊢ B \in dom R_{1} \to (A \in B \to R_{1} (A) \in R_{1} (B))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (B \in dom R_{1} \land A \in B) \to B \in dom R_{1}$
2		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
3	2	simpri	$⊢ Lim dom R_{1}$
4		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
5	3 4	ax-mp	$⊢ Ord dom R_{1}$
6		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
7	5 6	ax-mp	$⊢ dom R_{1} \subseteq On$
8	7	sseli	$⊢ B \in dom R_{1} \to B \in On$
9	1 8	syl	$⊢ (B \in dom R_{1} \land A \in B) \to B \in On$
10		onelon	$⊢ (B \in On \land A \in B) \to A \in On$
11	8 10	sylan	$⊢ (B \in dom R_{1} \land A \in B) \to A \in On$
12		suceloni	$⊢ A \in On \to suc A \in On$
13	11 12	syl	$⊢ (B \in dom R_{1} \land A \in B) \to suc A \in On$
14		eloni	$⊢ B \in On \to Ord B$
15		ordsucss	$⊢ Ord B \to (A \in B \to suc A \subseteq B)$
16	14 15	syl	$⊢ B \in On \to (A \in B \to suc A \subseteq B)$
17	16	imp	$⊢ (B \in On \land A \in B) \to suc A \subseteq B$
18	8 17	sylan	$⊢ (B \in dom R_{1} \land A \in B) \to suc A \subseteq B$
19		eleq1	$⊢ x = suc A \to (x \in dom R_{1} \leftrightarrow suc A \in dom R_{1})$
20		fveq2	$⊢ x = suc A \to R_{1} (x) = R_{1} (suc A)$
21	20	eleq2d	$⊢ x = suc A \to (R_{1} (A) \in R_{1} (x) \leftrightarrow R_{1} (A) \in R_{1} (suc A))$
22	19 21	imbi12d	$⊢ x = suc A \to ((x \in dom R_{1} \to R_{1} (A) \in R_{1} (x)) \leftrightarrow (suc A \in dom R_{1} \to R_{1} (A) \in R_{1} (suc A)))$
23		eleq1	$⊢ x = y \to (x \in dom R_{1} \leftrightarrow y \in dom R_{1})$
24		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
25	24	eleq2d	$⊢ x = y \to (R_{1} (A) \in R_{1} (x) \leftrightarrow R_{1} (A) \in R_{1} (y))$
26	23 25	imbi12d	$⊢ x = y \to ((x \in dom R_{1} \to R_{1} (A) \in R_{1} (x)) \leftrightarrow (y \in dom R_{1} \to R_{1} (A) \in R_{1} (y)))$
27		eleq1	$⊢ x = suc y \to (x \in dom R_{1} \leftrightarrow suc y \in dom R_{1})$
28		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
29	28	eleq2d	$⊢ x = suc y \to (R_{1} (A) \in R_{1} (x) \leftrightarrow R_{1} (A) \in R_{1} (suc y))$
30	27 29	imbi12d	$⊢ x = suc y \to ((x \in dom R_{1} \to R_{1} (A) \in R_{1} (x)) \leftrightarrow (suc y \in dom R_{1} \to R_{1} (A) \in R_{1} (suc y)))$
31		eleq1	$⊢ x = B \to (x \in dom R_{1} \leftrightarrow B \in dom R_{1})$
32		fveq2	$⊢ x = B \to R_{1} (x) = R_{1} (B)$
33	32	eleq2d	$⊢ x = B \to (R_{1} (A) \in R_{1} (x) \leftrightarrow R_{1} (A) \in R_{1} (B))$
34	31 33	imbi12d	$⊢ x = B \to ((x \in dom R_{1} \to R_{1} (A) \in R_{1} (x)) \leftrightarrow (B \in dom R_{1} \to R_{1} (A) \in R_{1} (B)))$
35		fvex	$⊢ R_{1} (A) \in V$
36	35	pwid	$⊢ R_{1} (A) \in 𝒫 R_{1} (A)$
37		limsuc	$⊢ Lim dom R_{1} \to (A \in dom R_{1} \leftrightarrow suc A \in dom R_{1})$
38	3 37	ax-mp	$⊢ A \in dom R_{1} \leftrightarrow suc A \in dom R_{1}$
39		r1sucg	$⊢ A \in dom R_{1} \to R_{1} (suc A) = 𝒫 R_{1} (A)$
40	38 39	sylbir	$⊢ suc A \in dom R_{1} \to R_{1} (suc A) = 𝒫 R_{1} (A)$
41	36 40	eleqtrrid	$⊢ suc A \in dom R_{1} \to R_{1} (A) \in R_{1} (suc A)$
42	41	a1i	$⊢ suc A \in On \to (suc A \in dom R_{1} \to R_{1} (A) \in R_{1} (suc A))$
43		limsuc	$⊢ Lim dom R_{1} \to (y \in dom R_{1} \leftrightarrow suc y \in dom R_{1})$
44	3 43	ax-mp	$⊢ y \in dom R_{1} \leftrightarrow suc y \in dom R_{1}$
45		r1tr	$⊢ Tr R_{1} (y)$
46		dftr4	$⊢ Tr R_{1} (y) \leftrightarrow R_{1} (y) \subseteq 𝒫 R_{1} (y)$
47	45 46	mpbi	$⊢ R_{1} (y) \subseteq 𝒫 R_{1} (y)$
48		r1sucg	$⊢ y \in dom R_{1} \to R_{1} (suc y) = 𝒫 R_{1} (y)$
49	47 48	sseqtrrid	$⊢ y \in dom R_{1} \to R_{1} (y) \subseteq R_{1} (suc y)$
50	49	sseld	$⊢ y \in dom R_{1} \to (R_{1} (A) \in R_{1} (y) \to R_{1} (A) \in R_{1} (suc y))$
51	50	a2i	$⊢ (y \in dom R_{1} \to R_{1} (A) \in R_{1} (y)) \to (y \in dom R_{1} \to R_{1} (A) \in R_{1} (suc y))$
52	44 51	syl5bir	$⊢ (y \in dom R_{1} \to R_{1} (A) \in R_{1} (y)) \to (suc y \in dom R_{1} \to R_{1} (A) \in R_{1} (suc y))$
53	52	a1i	$⊢ ((y \in On \land suc A \in On) \land suc A \subseteq y) \to ((y \in dom R_{1} \to R_{1} (A) \in R_{1} (y)) \to (suc y \in dom R_{1} \to R_{1} (A) \in R_{1} (suc y)))$
54		simprl	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to suc A \subseteq x$
55		simplr	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to suc A \in On$
56		sucelon	$⊢ A \in On \leftrightarrow suc A \in On$
57	55 56	sylibr	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to A \in On$
58		limord	$⊢ Lim x \to Ord x$
59	58	ad2antrr	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to Ord x$
60		ordelsuc	$⊢ (A \in On \land Ord x) \to (A \in x \leftrightarrow suc A \subseteq x)$
61	57 59 60	syl2anc	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to (A \in x \leftrightarrow suc A \subseteq x)$
62	54 61	mpbird	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to A \in x$
63		limsuc	$⊢ Lim x \to (A \in x \leftrightarrow suc A \in x)$
64	63	ad2antrr	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to (A \in x \leftrightarrow suc A \in x)$
65	62 64	mpbid	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to suc A \in x$
66		simprr	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to x \in dom R_{1}$
67		ordtr1	$⊢ Ord dom R_{1} \to ((A \in x \land x \in dom R_{1}) \to A \in dom R_{1})$
68	5 67	ax-mp	$⊢ (A \in x \land x \in dom R_{1}) \to A \in dom R_{1}$
69	62 66 68	syl2anc	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to A \in dom R_{1}$
70	69 39	syl	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to R_{1} (suc A) = 𝒫 R_{1} (A)$
71	36 70	eleqtrrid	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to R_{1} (A) \in R_{1} (suc A)$
72		fveq2	$⊢ y = suc A \to R_{1} (y) = R_{1} (suc A)$
73	72	eleq2d	$⊢ y = suc A \to (R_{1} (A) \in R_{1} (y) \leftrightarrow R_{1} (A) \in R_{1} (suc A))$
74	73	rspcev	$⊢ (suc A \in x \land R_{1} (A) \in R_{1} (suc A)) \to \exists y \in x R_{1} (A) \in R_{1} (y)$
75	65 71 74	syl2anc	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to \exists y \in x R_{1} (A) \in R_{1} (y)$
76		eliun	$⊢ R_{1} (A) \in ⋃_{y \in x} R_{1} (y) \leftrightarrow \exists y \in x R_{1} (A) \in R_{1} (y)$
77	75 76	sylibr	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to R_{1} (A) \in ⋃_{y \in x} R_{1} (y)$
78		simpll	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to Lim x$
79		r1limg	$⊢ (x \in dom R_{1} \land Lim x) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
80	66 78 79	syl2anc	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
81	77 80	eleqtrrd	$⊢ ((Lim x \land suc A \in On) \land (suc A \subseteq x \land x \in dom R_{1})) \to R_{1} (A) \in R_{1} (x)$
82	81	expr	$⊢ ((Lim x \land suc A \in On) \land suc A \subseteq x) \to (x \in dom R_{1} \to R_{1} (A) \in R_{1} (x))$
83	82	a1d	$⊢ ((Lim x \land suc A \in On) \land suc A \subseteq x) \to (\forall y \in x (suc A \subseteq y \to (y \in dom R_{1} \to R_{1} (A) \in R_{1} (y))) \to (x \in dom R_{1} \to R_{1} (A) \in R_{1} (x)))$
84	22 26 30 34 42 53 83	tfindsg	$⊢ ((B \in On \land suc A \in On) \land suc A \subseteq B) \to (B \in dom R_{1} \to R_{1} (A) \in R_{1} (B))$
85	84	impr	$⊢ ((B \in On \land suc A \in On) \land (suc A \subseteq B \land B \in dom R_{1})) \to R_{1} (A) \in R_{1} (B)$
86	9 13 18 1 85	syl22anc	$⊢ (B \in dom R_{1} \land A \in B) \to R_{1} (A) \in R_{1} (B)$
87	86	ex	$⊢ B \in dom R_{1} \to (A \in B \to R_{1} (A) \in R_{1} (B))$

Metamath Proof Explorer

Theorem r1ordg

Proof