r1sdom

Description: Each stage of the cumulative hierarchy of sets is strictly larger than any previous stage. (Contributed by Mario Carneiro, 19-Apr-2013)

		Ref	Expression
	Assertion	r1sdom	$⊢ (A \in On \land B \in A) \to R_{1} (B) ≺ R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ x = \emptyset \to (B \in x \leftrightarrow B \in \emptyset)$
2		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
3	2	breq2d	$⊢ x = \emptyset \to (R_{1} (B) ≺ R_{1} (x) \leftrightarrow R_{1} (B) ≺ R_{1} (\emptyset))$
4	1 3	imbi12d	$⊢ x = \emptyset \to ((B \in x \to R_{1} (B) ≺ R_{1} (x)) \leftrightarrow (B \in \emptyset \to R_{1} (B) ≺ R_{1} (\emptyset)))$
5		eleq2	$⊢ x = y \to (B \in x \leftrightarrow B \in y)$
6		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
7	6	breq2d	$⊢ x = y \to (R_{1} (B) ≺ R_{1} (x) \leftrightarrow R_{1} (B) ≺ R_{1} (y))$
8	5 7	imbi12d	$⊢ x = y \to ((B \in x \to R_{1} (B) ≺ R_{1} (x)) \leftrightarrow (B \in y \to R_{1} (B) ≺ R_{1} (y)))$
9		eleq2	$⊢ x = suc y \to (B \in x \leftrightarrow B \in suc y)$
10		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
11	10	breq2d	$⊢ x = suc y \to (R_{1} (B) ≺ R_{1} (x) \leftrightarrow R_{1} (B) ≺ R_{1} (suc y))$
12	9 11	imbi12d	$⊢ x = suc y \to ((B \in x \to R_{1} (B) ≺ R_{1} (x)) \leftrightarrow (B \in suc y \to R_{1} (B) ≺ R_{1} (suc y)))$
13		eleq2	$⊢ x = A \to (B \in x \leftrightarrow B \in A)$
14		fveq2	$⊢ x = A \to R_{1} (x) = R_{1} (A)$
15	14	breq2d	$⊢ x = A \to (R_{1} (B) ≺ R_{1} (x) \leftrightarrow R_{1} (B) ≺ R_{1} (A))$
16	13 15	imbi12d	$⊢ x = A \to ((B \in x \to R_{1} (B) ≺ R_{1} (x)) \leftrightarrow (B \in A \to R_{1} (B) ≺ R_{1} (A)))$
17		noel	$⊢ \neg B \in \emptyset$
18	17	pm2.21i	$⊢ B \in \emptyset \to R_{1} (B) ≺ R_{1} (\emptyset)$
19		elsuci	$⊢ B \in suc y \to (B \in y \lor B = y)$
20		sdomtr	$⊢ (R_{1} (B) ≺ R_{1} (y) \land R_{1} (y) ≺ R_{1} (suc y)) \to R_{1} (B) ≺ R_{1} (suc y)$
21	20	expcom	$⊢ R_{1} (y) ≺ R_{1} (suc y) \to (R_{1} (B) ≺ R_{1} (y) \to R_{1} (B) ≺ R_{1} (suc y))$
22		fvex	$⊢ R_{1} (y) \in V$
23	22	canth2	$⊢ R_{1} (y) ≺ 𝒫 R_{1} (y)$
24		r1suc	$⊢ y \in On \to R_{1} (suc y) = 𝒫 R_{1} (y)$
25	23 24	breqtrrid	$⊢ y \in On \to R_{1} (y) ≺ R_{1} (suc y)$
26	21 25	syl11	$⊢ R_{1} (B) ≺ R_{1} (y) \to (y \in On \to R_{1} (B) ≺ R_{1} (suc y))$
27	26	imim2i	$⊢ (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to (B \in y \to (y \in On \to R_{1} (B) ≺ R_{1} (suc y)))$
28		fveq2	$⊢ B = y \to R_{1} (B) = R_{1} (y)$
29	28	breq1d	$⊢ B = y \to (R_{1} (B) ≺ R_{1} (suc y) \leftrightarrow R_{1} (y) ≺ R_{1} (suc y))$
30	25 29	imbitrrid	$⊢ B = y \to (y \in On \to R_{1} (B) ≺ R_{1} (suc y))$
31	30	a1i	$⊢ (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to (B = y \to (y \in On \to R_{1} (B) ≺ R_{1} (suc y)))$
32	27 31	jaod	$⊢ (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to ((B \in y \lor B = y) \to (y \in On \to R_{1} (B) ≺ R_{1} (suc y)))$
33	19 32	syl5	$⊢ (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to (B \in suc y \to (y \in On \to R_{1} (B) ≺ R_{1} (suc y)))$
34	33	com3r	$⊢ y \in On \to ((B \in y \to R_{1} (B) ≺ R_{1} (y)) \to (B \in suc y \to R_{1} (B) ≺ R_{1} (suc y)))$
35		limuni	$⊢ Lim x \to x = ⋃ x$
36	35	eleq2d	$⊢ Lim x \to (B \in x \leftrightarrow B \in ⋃ x)$
37		eluni2	$⊢ B \in ⋃ x \leftrightarrow \exists y \in x B \in y$
38	36 37	bitrdi	$⊢ Lim x \to (B \in x \leftrightarrow \exists y \in x B \in y)$
39		r19.29	$⊢ (\forall y \in x (B \in y \to R_{1} (B) ≺ R_{1} (y)) \land \exists y \in x B \in y) \to \exists y \in x ((B \in y \to R_{1} (B) ≺ R_{1} (y)) \land B \in y)$
40		fvex	$⊢ R_{1} (x) \in V$
41		ssiun2	$⊢ y \in x \to R_{1} (y) \subseteq ⋃_{y \in x} R_{1} (y)$
42		vex	$⊢ x \in V$
43		r1lim	$⊢ (x \in V \land Lim x) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
44	42 43	mpan	$⊢ Lim x \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
45	44	sseq2d	$⊢ Lim x \to (R_{1} (y) \subseteq R_{1} (x) \leftrightarrow R_{1} (y) \subseteq ⋃_{y \in x} R_{1} (y))$
46	41 45	imbitrrid	$⊢ Lim x \to (y \in x \to R_{1} (y) \subseteq R_{1} (x))$
47		ssdomg	$⊢ R_{1} (x) \in V \to (R_{1} (y) \subseteq R_{1} (x) \to R_{1} (y) ≼ R_{1} (x))$
48	40 46 47	mpsylsyld	$⊢ Lim x \to (y \in x \to R_{1} (y) ≼ R_{1} (x))$
49		id	$⊢ (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to (B \in y \to R_{1} (B) ≺ R_{1} (y))$
50	49	imp	$⊢ ((B \in y \to R_{1} (B) ≺ R_{1} (y)) \land B \in y) \to R_{1} (B) ≺ R_{1} (y)$
51		sdomdomtr	$⊢ (R_{1} (B) ≺ R_{1} (y) \land R_{1} (y) ≼ R_{1} (x)) \to R_{1} (B) ≺ R_{1} (x)$
52	51	expcom	$⊢ R_{1} (y) ≼ R_{1} (x) \to (R_{1} (B) ≺ R_{1} (y) \to R_{1} (B) ≺ R_{1} (x))$
53	50 52	syl5	$⊢ R_{1} (y) ≼ R_{1} (x) \to (((B \in y \to R_{1} (B) ≺ R_{1} (y)) \land B \in y) \to R_{1} (B) ≺ R_{1} (x))$
54	48 53	syl6	$⊢ Lim x \to (y \in x \to (((B \in y \to R_{1} (B) ≺ R_{1} (y)) \land B \in y) \to R_{1} (B) ≺ R_{1} (x)))$
55	54	rexlimdv	$⊢ Lim x \to (\exists y \in x ((B \in y \to R_{1} (B) ≺ R_{1} (y)) \land B \in y) \to R_{1} (B) ≺ R_{1} (x))$
56	39 55	syl5	$⊢ Lim x \to ((\forall y \in x (B \in y \to R_{1} (B) ≺ R_{1} (y)) \land \exists y \in x B \in y) \to R_{1} (B) ≺ R_{1} (x))$
57	56	expcomd	$⊢ Lim x \to (\exists y \in x B \in y \to (\forall y \in x (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to R_{1} (B) ≺ R_{1} (x)))$
58	38 57	sylbid	$⊢ Lim x \to (B \in x \to (\forall y \in x (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to R_{1} (B) ≺ R_{1} (x)))$
59	58	com23	$⊢ Lim x \to (\forall y \in x (B \in y \to R_{1} (B) ≺ R_{1} (y)) \to (B \in x \to R_{1} (B) ≺ R_{1} (x)))$
60	4 8 12 16 18 34 59	tfinds	$⊢ A \in On \to (B \in A \to R_{1} (B) ≺ R_{1} (A))$
61	60	imp	$⊢ (A \in On \land B \in A) \to R_{1} (B) ≺ R_{1} (A)$

Metamath Proof Explorer

Theorem r1sdom

Proof