rankonidlem

Description: Lemma for rankonid . (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 22-Mar-2013)

		Ref	Expression
	Assertion	rankonidlem	$⊢ A \in dom R_{1} \to (A \in ⋃ R_{1} [On] \land rank (A) = A)$

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	$⊢ Lim dom R_{1}$
2		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
3	1 2	ax-mp	$⊢ Ord dom R_{1}$
4		ordelon	$⊢ (Ord dom R_{1} \land A \in dom R_{1}) \to A \in On$
5	3 4	mpan	$⊢ A \in dom R_{1} \to A \in On$
6		eleq1	$⊢ x = y \to (x \in dom R_{1} \leftrightarrow y \in dom R_{1})$
7		eleq1	$⊢ x = y \to (x \in ⋃ R_{1} [On] \leftrightarrow y \in ⋃ R_{1} [On])$
8		fveq2	$⊢ x = y \to rank (x) = rank (y)$
9		id	$⊢ x = y \to x = y$
10	8 9	eqeq12d	$⊢ x = y \to (rank (x) = x \leftrightarrow rank (y) = y)$
11	7 10	anbi12d	$⊢ x = y \to ((x \in ⋃ R_{1} [On] \land rank (x) = x) \leftrightarrow (y \in ⋃ R_{1} [On] \land rank (y) = y))$
12	6 11	imbi12d	$⊢ x = y \to ((x \in dom R_{1} \to (x \in ⋃ R_{1} [On] \land rank (x) = x)) \leftrightarrow (y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)))$
13		eleq1	$⊢ x = A \to (x \in dom R_{1} \leftrightarrow A \in dom R_{1})$
14		eleq1	$⊢ x = A \to (x \in ⋃ R_{1} [On] \leftrightarrow A \in ⋃ R_{1} [On])$
15		fveq2	$⊢ x = A \to rank (x) = rank (A)$
16		id	$⊢ x = A \to x = A$
17	15 16	eqeq12d	$⊢ x = A \to (rank (x) = x \leftrightarrow rank (A) = A)$
18	14 17	anbi12d	$⊢ x = A \to ((x \in ⋃ R_{1} [On] \land rank (x) = x) \leftrightarrow (A \in ⋃ R_{1} [On] \land rank (A) = A))$
19	13 18	imbi12d	$⊢ x = A \to ((x \in dom R_{1} \to (x \in ⋃ R_{1} [On] \land rank (x) = x)) \leftrightarrow (A \in dom R_{1} \to (A \in ⋃ R_{1} [On] \land rank (A) = A)))$
20		ordtr1	$⊢ Ord dom R_{1} \to ((y \in x \land x \in dom R_{1}) \to y \in dom R_{1})$
21	3 20	ax-mp	$⊢ (y \in x \land x \in dom R_{1}) \to y \in dom R_{1}$
22	21	ancoms	$⊢ (x \in dom R_{1} \land y \in x) \to y \in dom R_{1}$
23		pm5.5	$⊢ y \in dom R_{1} \to ((y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)) \leftrightarrow (y \in ⋃ R_{1} [On] \land rank (y) = y))$
24	22 23	syl	$⊢ (x \in dom R_{1} \land y \in x) \to ((y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)) \leftrightarrow (y \in ⋃ R_{1} [On] \land rank (y) = y))$
25	24	ralbidva	$⊢ x \in dom R_{1} \to (\forall y \in x (y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)) \leftrightarrow \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y))$
26		simplr	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to y \in x$
27		ordelon	$⊢ (Ord dom R_{1} \land x \in dom R_{1}) \to x \in On$
28	3 27	mpan	$⊢ x \in dom R_{1} \to x \in On$
29	28	ad2antrr	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in On$
30		eloni	$⊢ x \in On \to Ord x$
31	29 30	syl	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to Ord x$
32		ordelsuc	$⊢ (y \in x \land Ord x) \to (y \in x \leftrightarrow suc y \subseteq x)$
33	26 31 32	syl2anc	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to (y \in x \leftrightarrow suc y \subseteq x)$
34	26 33	mpbid	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to suc y \subseteq x$
35	22	adantr	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to y \in dom R_{1}$
36		limsuc	$⊢ Lim dom R_{1} \to (y \in dom R_{1} \leftrightarrow suc y \in dom R_{1})$
37	1 36	ax-mp	$⊢ y \in dom R_{1} \leftrightarrow suc y \in dom R_{1}$
38	35 37	sylib	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to suc y \in dom R_{1}$
39		simpll	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in dom R_{1}$
40		r1ord3g	$⊢ (suc y \in dom R_{1} \land x \in dom R_{1}) \to (suc y \subseteq x \to R_{1} (suc y) \subseteq R_{1} (x))$
41	38 39 40	syl2anc	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to (suc y \subseteq x \to R_{1} (suc y) \subseteq R_{1} (x))$
42	34 41	mpd	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to R_{1} (suc y) \subseteq R_{1} (x)$
43		rankidb	$⊢ y \in ⋃ R_{1} [On] \to y \in R_{1} (suc rank (y))$
44	43	ad2antrl	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to y \in R_{1} (suc rank (y))$
45		suceq	$⊢ rank (y) = y \to suc rank (y) = suc y$
46	45	ad2antll	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to suc rank (y) = suc y$
47	46	fveq2d	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to R_{1} (suc rank (y)) = R_{1} (suc y)$
48	44 47	eleqtrd	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to y \in R_{1} (suc y)$
49	42 48	sseldd	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to y \in R_{1} (x)$
50	49	ex	$⊢ (x \in dom R_{1} \land y \in x) \to ((y \in ⋃ R_{1} [On] \land rank (y) = y) \to y \in R_{1} (x))$
51	50	ralimdva	$⊢ x \in dom R_{1} \to (\forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to \forall y \in x y \in R_{1} (x))$
52	51	imp	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to \forall y \in x y \in R_{1} (x)$
53		dfss3	$⊢ x \subseteq R_{1} (x) \leftrightarrow \forall y \in x y \in R_{1} (x)$
54	52 53	sylibr	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \subseteq R_{1} (x)$
55		vex	$⊢ x \in V$
56	55	elpw	$⊢ x \in 𝒫 R_{1} (x) \leftrightarrow x \subseteq R_{1} (x)$
57	54 56	sylibr	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in 𝒫 R_{1} (x)$
58		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
59	58	adantr	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
60	57 59	eleqtrrd	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in R_{1} (suc x)$
61		r1elwf	$⊢ x \in R_{1} (suc x) \to x \in ⋃ R_{1} [On]$
62	60 61	syl	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in ⋃ R_{1} [On]$
63		rankval3b	$⊢ x \in ⋃ R_{1} [On] \to rank (x) = ⋂ \{z \in On \| \forall y \in x rank (y) \in z\}$
64	62 63	syl	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to rank (x) = ⋂ \{z \in On \| \forall y \in x rank (y) \in z\}$
65		eleq1	$⊢ rank (y) = y \to (rank (y) \in z \leftrightarrow y \in z)$
66	65	adantl	$⊢ (y \in ⋃ R_{1} [On] \land rank (y) = y) \to (rank (y) \in z \leftrightarrow y \in z)$
67	66	ralimi	$⊢ \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to \forall y \in x (rank (y) \in z \leftrightarrow y \in z)$
68		ralbi	$⊢ \forall y \in x (rank (y) \in z \leftrightarrow y \in z) \to (\forall y \in x rank (y) \in z \leftrightarrow \forall y \in x y \in z)$
69	67 68	syl	$⊢ \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to (\forall y \in x rank (y) \in z \leftrightarrow \forall y \in x y \in z)$
70		dfss3	$⊢ x \subseteq z \leftrightarrow \forall y \in x y \in z$
71	69 70	bitr4di	$⊢ \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to (\forall y \in x rank (y) \in z \leftrightarrow x \subseteq z)$
72	71	rabbidv	$⊢ \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to \{z \in On \| \forall y \in x rank (y) \in z\} = \{z \in On \| x \subseteq z\}$
73	72	inteqd	$⊢ \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to ⋂ \{z \in On \| \forall y \in x rank (y) \in z\} = ⋂ \{z \in On \| x \subseteq z\}$
74	73	adantl	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to ⋂ \{z \in On \| \forall y \in x rank (y) \in z\} = ⋂ \{z \in On \| x \subseteq z\}$
75	28	adantr	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in On$
76		intmin	$⊢ x \in On \to ⋂ \{z \in On \| x \subseteq z\} = x$
77	75 76	syl	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to ⋂ \{z \in On \| x \subseteq z\} = x$
78	64 74 77	3eqtrd	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to rank (x) = x$
79	62 78	jca	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to (x \in ⋃ R_{1} [On] \land rank (x) = x)$
80	79	ex	$⊢ x \in dom R_{1} \to (\forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y) \to (x \in ⋃ R_{1} [On] \land rank (x) = x))$
81	25 80	sylbid	$⊢ x \in dom R_{1} \to (\forall y \in x (y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to (x \in ⋃ R_{1} [On] \land rank (x) = x))$
82	81	com12	$⊢ \forall y \in x (y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to (x \in dom R_{1} \to (x \in ⋃ R_{1} [On] \land rank (x) = x))$
83	82	a1i	$⊢ x \in On \to (\forall y \in x (y \in dom R_{1} \to (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to (x \in dom R_{1} \to (x \in ⋃ R_{1} [On] \land rank (x) = x)))$
84	12 19 83	tfis3	$⊢ A \in On \to (A \in dom R_{1} \to (A \in ⋃ R_{1} [On] \land rank (A) = A))$
85	5 84	mpcom	$⊢ A \in dom R_{1} \to (A \in ⋃ R_{1} [On] \land rank (A) = A)$

Metamath Proof Explorer

Theorem rankonidlem

Proof