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

Metamath Proof Explorer

Theorem r1ordg

Proof