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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
2	1	simpri	$⊢ 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		ordelon	$⊢ (Ord dom R_{1} \land A \in dom R_{1}) \to A \in On$
6	4 5	mpan	$⊢ A \in dom R_{1} \to A \in On$
7		eleq1	$⊢ x = y \to (x \in dom R_{1} \leftrightarrow y \in dom R_{1})$
8		eleq1	$⊢ x = y \to (x \in ⋃ R_{1} [On] \leftrightarrow y \in ⋃ R_{1} [On])$
9		fveq2	$⊢ x = y \to rank (x) = rank (y)$
10		id	$⊢ x = y \to x = y$
11	9 10	eqeq12d	$⊢ x = y \to (rank (x) = x \leftrightarrow rank (y) = y)$
12	8 11	anbi12d	$⊢ x = y \to ((x \in ⋃ R_{1} [On] \land rank (x) = x) \leftrightarrow (y \in ⋃ R_{1} [On] \land rank (y) = y))$
13	7 12	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)))$
14		eleq1	$⊢ x = A \to (x \in dom R_{1} \leftrightarrow A \in dom R_{1})$
15		eleq1	$⊢ x = A \to (x \in ⋃ R_{1} [On] \leftrightarrow A \in ⋃ R_{1} [On])$
16		fveq2	$⊢ x = A \to rank (x) = rank (A)$
17		id	$⊢ x = A \to x = A$
18	16 17	eqeq12d	$⊢ x = A \to (rank (x) = x \leftrightarrow rank (A) = A)$
19	15 18	anbi12d	$⊢ x = A \to ((x \in ⋃ R_{1} [On] \land rank (x) = x) \leftrightarrow (A \in ⋃ R_{1} [On] \land rank (A) = A))$
20	14 19	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)))$
21		ordtr1	$⊢ Ord dom R_{1} \to ((y \in x \land x \in dom R_{1}) \to y \in dom R_{1})$
22	4 21	ax-mp	$⊢ (y \in x \land x \in dom R_{1}) \to y \in dom R_{1}$
23	22	ancoms	$⊢ (x \in dom R_{1} \land y \in x) \to y \in dom R_{1}$
24		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))$
25	23 24	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))$
26	25	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))$
27		simplr	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to y \in x$
28		ordelon	$⊢ (Ord dom R_{1} \land x \in dom R_{1}) \to x \in On$
29	4 28	mpan	$⊢ x \in dom R_{1} \to x \in On$
30	29	ad2antrr	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in On$
31		eloni	$⊢ x \in On \to Ord x$
32	30 31	syl	$⊢ ((x \in dom R_{1} \land y \in x) \land (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to Ord x$
33		ordelsuc	$⊢ (y \in x \land Ord x) \to (y \in x \leftrightarrow suc y \subseteq x)$
34	27 32 33	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)$
35	27 34	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$
36	23	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}$
37		limsuc	$⊢ Lim dom R_{1} \to (y \in dom R_{1} \leftrightarrow suc y \in dom R_{1})$
38	2 37	ax-mp	$⊢ y \in dom R_{1} \leftrightarrow suc y \in dom R_{1}$
39	36 38	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}$
40		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}$
41		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))$
42	39 40 41	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))$
43	35 42	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)$
44		rankidb	$⊢ y \in ⋃ R_{1} [On] \to y \in R_{1} (suc rank (y))$
45	44	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))$
46		suceq	$⊢ rank (y) = y \to suc rank (y) = suc y$
47	46	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$
48	47	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)$
49	45 48	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)$
50	43 49	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)$
51	50	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))$
52	51	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))$
53	52	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)$
54		dfss3	$⊢ x \subseteq R_{1} (x) \leftrightarrow \forall y \in x y \in R_{1} (x)$
55	53 54	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)$
56		vex	$⊢ x \in V$
57	56	elpw	$⊢ x \in 𝒫 R_{1} (x) \leftrightarrow x \subseteq R_{1} (x)$
58	55 57	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)$
59		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
60	59	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)$
61	58 60	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)$
62		r1elwf	$⊢ x \in R_{1} (suc x) \to x \in ⋃ R_{1} [On]$
63	61 62	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]$
64		rankval3b	$⊢ x \in ⋃ R_{1} [On] \to rank (x) = ⋂ \{z \in On \| \forall y \in x rank (y) \in z\}$
65	63 64	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\}$
66		eleq1	$⊢ rank (y) = y \to (rank (y) \in z \leftrightarrow y \in z)$
67	66	adantl	$⊢ (y \in ⋃ R_{1} [On] \land rank (y) = y) \to (rank (y) \in z \leftrightarrow y \in z)$
68	67	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)$
69		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)$
70	68 69	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)$
71		dfss3	$⊢ x \subseteq z \leftrightarrow \forall y \in x y \in z$
72	70 71	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)$
73	72	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\}$
74	73	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\}$
75	74	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\}$
76	29	adantr	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to x \in On$
77		intmin	$⊢ x \in On \to ⋂ \{z \in On \| x \subseteq z\} = x$
78	76 77	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$
79	65 75 78	3eqtrd	$⊢ (x \in dom R_{1} \land \forall y \in x (y \in ⋃ R_{1} [On] \land rank (y) = y)) \to rank (x) = x$
80	63 79	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)$
81	80	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))$
82	26 81	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))$
83	82	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))$
84	83	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)))$
85	13 20 84	tfis3	$⊢ A \in On \to (A \in dom R_{1} \to (A \in ⋃ R_{1} [On] \land rank (A) = A))$
86	6 85	mpcom	$⊢ A \in dom R_{1} \to (A \in ⋃ R_{1} [On] \land rank (A) = A)$

Metamath Proof Explorer

Theorem rankonidlem

Proof