Theorem rankr1 4736

Description: A relationship between the rank function and the cumulative hierarchy of sets function R₁. Proposition 9.15(2) of [TakeutiZaring] p. 79.

Hypothesis

Ref	Expression
rankr1.1	⊢ A ∈ V

Assertion

Ref	Expression
rankr1	⊢ (B = (rank ‘A) ↔ (¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)))

Proof of Theorem rankr1

Step	Hyp	Ref	Expression
1		rankon 4733	. . . . 5 ⊢ (rank ‘A) ∈ On
2		eleq1 1581	. . . . 5 ⊢ (B = (rank ‘A) → (B ∈ On ↔ (rank ‘A) ∈ On))
3	1, 2	mpbiri 201	. . . 4 ⊢ (B = (rank ‘A) → B ∈ On)
4		eloni 3015	. . . . 5 ⊢ (B ∈ On → Ord B)
5		ordzsl 3173	. . . . . 6 ⊢ (Ord B ↔ (B = ∅ ⋁ ∃x ∈ On B = suc x ⋁ Lim B))
6		noel 2335	. . . . . . . . 9 ⊢ ¬ A ∈ ∅
7		fveq2 3781	. . . . . . . . . . 11 ⊢ (B = ∅ → (R1 ‘B) = (R1 ‘∅))
8		r10 4713	. . . . . . . . . . 11 ⊢ (R1 ‘∅) = ∅
9	7, 8	syl6eq 1570	. . . . . . . . . 10 ⊢ (B = ∅ → (R1 ‘B) = ∅)
10	9	eleq2d 1588	. . . . . . . . 9 ⊢ (B = ∅ → (A ∈ (R1 ‘B) ↔ A ∈ ∅))
11	6, 10	mtbiri 729	. . . . . . . 8 ⊢ (B = ∅ → ¬ A ∈ (R1 ‘B))
12	11	a1d 12	. . . . . . 7 ⊢ (B = ∅ → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B)))
13		visset 1860	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
14	13	sucid 3108	. . . . . . . . . . . . . 14 ⊢ x ∈ suc x
15		eleq2 1582	. . . . . . . . . . . . . 14 ⊢ (B = suc x → (x ∈ B ↔ x ∈ suc x))
16	14, 15	mpbiri 201	. . . . . . . . . . . . 13 ⊢ (B = suc x → x ∈ B)
17	16	adantl 397	. . . . . . . . . . . 12 ⊢ ((x ∈ On ⋀ B = suc x) → x ∈ B)
18		ontri1 3038	. . . . . . . . . . . . . 14 ⊢ ((B ∈ On ⋀ x ∈ On) → (B ⊆ x ↔ ¬ x ∈ B))
19	18	con2bid 537	. . . . . . . . . . . . 13 ⊢ ((B ∈ On ⋀ x ∈ On) → (x ∈ B ↔ ¬ B ⊆ x))
20		eleq1a 1590	. . . . . . . . . . . . . . 15 ⊢ (suc x ∈ On → (B = suc x → B ∈ On))
21	20	imp 357	. . . . . . . . . . . . . 14 ⊢ ((suc x ∈ On ⋀ B = suc x) → B ∈ On)
22		suceloni 3119	. . . . . . . . . . . . . 14 ⊢ (x ∈ On → suc x ∈ On)
23	21, 22	sylan 459	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ⋀ B = suc x) → B ∈ On)
24		pm3.26 326	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ⋀ B = suc x) → x ∈ On)
25	19, 23, 24	sylanc 482	. . . . . . . . . . . 12 ⊢ ((x ∈ On ⋀ B = suc x) → (x ∈ B ↔ ¬ B ⊆ x))
26	17, 25	mpbid 202	. . . . . . . . . . 11 ⊢ ((x ∈ On ⋀ B = suc x) → ¬ B ⊆ x)
27	26	adantr 398	. . . . . . . . . 10 ⊢ (((x ∈ On ⋀ B = suc x) ⋀ B = (rank ‘A)) → ¬ B ⊆ x)
28		rankr1.1	. . . . . . . . . . . . . . . . . . 19 ⊢ A ∈ V
29	28	rankval 4730	. . . . . . . . . . . . . . . . . 18 ⊢ (rank ‘A) = ∩{y ∈ On∣A ∈ (R1 ‘suc y)}
30	29	eqeq2i 1532	. . . . . . . . . . . . . . . . 17 ⊢ (B = (rank ‘A) ↔ B = ∩{y ∈ On∣A ∈ (R1 ‘suc y)})
31	30	biimpi 158	. . . . . . . . . . . . . . . 16 ⊢ (B = (rank ‘A) → B = ∩{y ∈ On∣A ∈ (R1 ‘suc y)})
32	31	sseq1d 2139	. . . . . . . . . . . . . . 15 ⊢ (B = (rank ‘A) → (B ⊆ x ↔ ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ x))
33		suceq 3091	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = x → suc y = suc x)
34	33	fveq2d 3785	. . . . . . . . . . . . . . . . . 18 ⊢ (y = x → (R1 ‘suc y) = (R1 ‘suc x))
35	34	eleq2d 1588	. . . . . . . . . . . . . . . . 17 ⊢ (y = x → (A ∈ (R1 ‘suc y) ↔ A ∈ (R1 ‘suc x)))
36	35	onintss 3068	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ On → (A ∈ (R1 ‘suc x) → ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ x))
37	36	imp 357	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On ⋀ A ∈ (R1 ‘suc x)) → ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ x)
38	32, 37	syl5bir 217	. . . . . . . . . . . . . 14 ⊢ (B = (rank ‘A) → ((x ∈ On ⋀ A ∈ (R1 ‘suc x)) → B ⊆ x))
39		fveq2 3781	. . . . . . . . . . . . . . . 16 ⊢ (B = suc x → (R1 ‘B) = (R1 ‘suc x))
40	39	eleq2d 1588	. . . . . . . . . . . . . . 15 ⊢ (B = suc x → (A ∈ (R1 ‘B) ↔ A ∈ (R1 ‘suc x)))
41	40	biimpa 425	. . . . . . . . . . . . . 14 ⊢ ((B = suc x ⋀ A ∈ (R1 ‘B)) → A ∈ (R1 ‘suc x))
42	38, 41	sylan2i 476	. . . . . . . . . . . . 13 ⊢ (B = (rank ‘A) → ((x ∈ On ⋀ (B = suc x ⋀ A ∈ (R1 ‘B))) → B ⊆ x))
43	42	exp4d 390	. . . . . . . . . . . 12 ⊢ (B = (rank ‘A) → (x ∈ On → (B = suc x → (A ∈ (R1 ‘B) → B ⊆ x))))
44	43	com3l 34	. . . . . . . . . . 11 ⊢ (x ∈ On → (B = suc x → (B = (rank ‘A) → (A ∈ (R1 ‘B) → B ⊆ x))))
45	44	imp31 369	. . . . . . . . . 10 ⊢ (((x ∈ On ⋀ B = suc x) ⋀ B = (rank ‘A)) → (A ∈ (R1 ‘B) → B ⊆ x))
46	27, 45	mtod 114	. . . . . . . . 9 ⊢ (((x ∈ On ⋀ B = suc x) ⋀ B = (rank ‘A)) → ¬ A ∈ (R1 ‘B))
47	46	exp31 385	. . . . . . . 8 ⊢ (x ∈ On → (B = suc x → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B))))
48	47	r19.23aiv 1790	. . . . . . 7 ⊢ (∃x ∈ On B = suc x → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B)))
49		eleq2 1582	. . . . . . . . . . . . . . . . . 18 ⊢ (B = (rank ‘A) → (x ∈ B ↔ x ∈ (rank ‘A)))
50	1	oneli 3155	. . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ (rank ‘A) → x ∈ On)
51	49, 50	syl6bi 221	. . . . . . . . . . . . . . . . 17 ⊢ (B = (rank ‘A) → (x ∈ B → x ∈ On))
52	51	anc2li 309	. . . . . . . . . . . . . . . 16 ⊢ (B = (rank ‘A) → (x ∈ B → (B = (rank ‘A) ⋀ x ∈ On)))
53		r1ord2 4718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc x ∈ On → (x ∈ suc x → (R1 ‘x) ⊆ (R1 ‘suc x)))
54	14, 53	mpi 44	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc x ∈ On → (R1 ‘x) ⊆ (R1 ‘suc x))
55	22, 54	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ∈ On → (R1 ‘x) ⊆ (R1 ‘suc x))
56	55	sseld 2118	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ∈ On → (A ∈ (R1 ‘x) → A ∈ (R1 ‘suc x)))
57	29	sseq1i 2136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((rank ‘A) ⊆ x ↔ ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ x)
58	36, 57	syl6ibr 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ∈ On → (A ∈ (R1 ‘suc x) → (rank ‘A) ⊆ x))
59	56, 58	syld 27	. . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ On → (A ∈ (R1 ‘x) → (rank ‘A) ⊆ x))
60		sseq1 2133	. . . . . . . . . . . . . . . . . . 19 ⊢ (B = (rank ‘A) → (B ⊆ x ↔ (rank ‘A) ⊆ x))
61	60	biimprd 161	. . . . . . . . . . . . . . . . . 18 ⊢ (B = (rank ‘A) → ((rank ‘A) ⊆ x → B ⊆ x))
62	59, 61	sylan9r 480	. . . . . . . . . . . . . . . . 17 ⊢ ((B = (rank ‘A) ⋀ x ∈ On) → (A ∈ (R1 ‘x) → B ⊆ x))
63	18, 3	sylan 459	. . . . . . . . . . . . . . . . 17 ⊢ ((B = (rank ‘A) ⋀ x ∈ On) → (B ⊆ x ↔ ¬ x ∈ B))
64	62, 63	sylibd 209	. . . . . . . . . . . . . . . 16 ⊢ ((B = (rank ‘A) ⋀ x ∈ On) → (A ∈ (R1 ‘x) → ¬ x ∈ B))
65	52, 64	syl6 22	. . . . . . . . . . . . . . 15 ⊢ (B = (rank ‘A) → (x ∈ B → (A ∈ (R1 ‘x) → ¬ x ∈ B)))
66	65	com3l 34	. . . . . . . . . . . . . 14 ⊢ (x ∈ B → (A ∈ (R1 ‘x) → (B = (rank ‘A) → ¬ x ∈ B)))
67		con2 94	. . . . . . . . . . . . . 14 ⊢ ((B = (rank ‘A) → ¬ x ∈ B) → (x ∈ B → ¬ B = (rank ‘A)))
68	66, 67	syl6 22	. . . . . . . . . . . . 13 ⊢ (x ∈ B → (A ∈ (R1 ‘x) → (x ∈ B → ¬ B = (rank ‘A))))
69	68	pm2.43a 68	. . . . . . . . . . . 12 ⊢ (x ∈ B → (A ∈ (R1 ‘x) → ¬ B = (rank ‘A)))
70	69	r19.23aiv 1790	. . . . . . . . . . 11 ⊢ (∃x ∈ B A ∈ (R1 ‘x) → ¬ B = (rank ‘A))
71	70	con2i 102	. . . . . . . . . 10 ⊢ (B = (rank ‘A) → ¬ ∃x ∈ B A ∈ (R1 ‘x))
72	71	adantr 398	. . . . . . . . 9 ⊢ ((B = (rank ‘A) ⋀ Lim B) → ¬ ∃x ∈ B A ∈ (R1 ‘x))
73		r1lim 4715	. . . . . . . . . . . 12 ⊢ ((B ∈ V ⋀ Lim B) → (R1 ‘B) = ∪x ∈ B (R1 ‘x))
74		fvex 3789	. . . . . . . . . . . . 13 ⊢ (rank ‘A) ∈ V
75		eleq1 1581	. . . . . . . . . . . . 13 ⊢ (B = (rank ‘A) → (B ∈ V ↔ (rank ‘A) ∈ V))
76	74, 75	mpbiri 201	. . . . . . . . . . . 12 ⊢ (B = (rank ‘A) → B ∈ V)
77	73, 76	sylan 459	. . . . . . . . . . 11 ⊢ ((B = (rank ‘A) ⋀ Lim B) → (R1 ‘B) = ∪x ∈ B (R1 ‘x))
78	77	eleq2d 1588	. . . . . . . . . 10 ⊢ ((B = (rank ‘A) ⋀ Lim B) → (A ∈ (R1 ‘B) ↔ A ∈ ∪x ∈ B (R1 ‘x)))
79		eliun 2624	. . . . . . . . . 10 ⊢ (A ∈ ∪x ∈ B (R1 ‘x) ↔ ∃x ∈ B A ∈ (R1 ‘x))
80	78, 79	syl6bb 547	. . . . . . . . 9 ⊢ ((B = (rank ‘A) ⋀ Lim B) → (A ∈ (R1 ‘B) ↔ ∃x ∈ B A ∈ (R1 ‘x)))
81	72, 80	mtbird 727	. . . . . . . 8 ⊢ ((B = (rank ‘A) ⋀ Lim B) → ¬ A ∈ (R1 ‘B))
82	81	expcom 381	. . . . . . 7 ⊢ (Lim B → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B)))
83	12, 48, 82	3jaoi 899	. . . . . 6 ⊢ ((B = ∅ ⋁ ∃x ∈ On B = suc x ⋁ Lim B) → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B)))
84	5, 83	sylbi 206	. . . . 5 ⊢ (Ord B → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B)))
85	4, 84	syl 10	. . . 4 ⊢ (B ∈ On → (B = (rank ‘A) → ¬ A ∈ (R1 ‘B)))
86	3, 85	mpcom 49	. . 3 ⊢ (B = (rank ‘A) → ¬ A ∈ (R1 ‘B))
87		ssrab2 2182	. . . . . . 7 ⊢ {y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ On
88		rankwflem 4727	. . . . . . . . 9 ⊢ (A ∈ V → ∃y ∈ On A ∈ (R1 ‘suc y))
89	28, 88	ax-mp 7	. . . . . . . 8 ⊢ ∃y ∈ On A ∈ (R1 ‘suc y)
90		rabn0 2344	. . . . . . . 8 ⊢ ({y ∈ On∣A ∈ (R1 ‘suc y)} ≠ ∅ ↔ ∃y ∈ On A ∈ (R1 ‘suc y))
91	89, 90	mpbir 197	. . . . . . 7 ⊢ {y ∈ On∣A ∈ (R1 ‘suc y)} ≠ ∅
92		onint 3063	. . . . . . 7 ⊢ (({y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ On ⋀ {y ∈ On∣A ∈ (R1 ‘suc y)} ≠ ∅) → ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ∈ {y ∈ On∣A ∈ (R1 ‘suc y)})
93	87, 91, 92	mp2an 709	. . . . . 6 ⊢ ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ∈ {y ∈ On∣A ∈ (R1 ‘suc y)}
94	29, 93	eqeltri 1591	. . . . 5 ⊢ (rank ‘A) ∈ {y ∈ On∣A ∈ (R1 ‘suc y)}
95		eleq1 1581	. . . . 5 ⊢ (B = (rank ‘A) → (B ∈ {y ∈ On∣A ∈ (R1 ‘suc y)} ↔ (rank ‘A) ∈ {y ∈ On∣A ∈ (R1 ‘suc y)}))
96	94, 95	mpbiri 201	. . . 4 ⊢ (B = (rank ‘A) → B ∈ {y ∈ On∣A ∈ (R1 ‘suc y)})
97		suceq 3091	. . . . . . . 8 ⊢ (y = B → suc y = suc B)
98	97	fveq2d 3785	. . . . . . 7 ⊢ (y = B → (R1 ‘suc y) = (R1 ‘suc B))
99	98	eleq2d 1588	. . . . . 6 ⊢ (y = B → (A ∈ (R1 ‘suc y) ↔ A ∈ (R1 ‘suc B)))
100	99	elrab 1952	. . . . 5 ⊢ (B ∈ {y ∈ On∣A ∈ (R1 ‘suc y)} ↔ (B ∈ On ⋀ A ∈ (R1 ‘suc B)))
101	100	pm3.27bi 333	. . . 4 ⊢ (B ∈ {y ∈ On∣A ∈ (R1 ‘suc y)} → A ∈ (R1 ‘suc B))
102	96, 101	syl 10	. . 3 ⊢ (B = (rank ‘A) → A ∈ (R1 ‘suc B))
103	86, 102	jca 295	. 2 ⊢ (B = (rank ‘A) → (¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)))
104	28	rankr1lem 4735	. . . . . 6 ⊢ (B ∈ On → (¬ A ∈ (R1 ‘B) → B ⊆ (rank ‘A)))
105	104	com12 11	. . . . 5 ⊢ (¬ A ∈ (R1 ‘B) → (B ∈ On → B ⊆ (rank ‘A)))
106		elfvdm 3804	. . . . . 6 ⊢ (A ∈ (R1 ‘suc B) → suc B ∈ dom R1)
107		r1fnon 4712	. . . . . . . . 9 ⊢ R1 Fn On
108		fndm 3644	. . . . . . . . 9 ⊢ (R1 Fn On → dom R1 = On)
109	107, 108	ax-mp 7	. . . . . . . 8 ⊢ dom R1 = On
110	109	eleq2i 1585	. . . . . . 7 ⊢ (suc B ∈ dom R1 ↔ suc B ∈ On)
111		sucelon 3125	. . . . . . 7 ⊢ (B ∈ On ↔ suc B ∈ On)
112	110, 111	bitr4i 183	. . . . . 6 ⊢ (suc B ∈ dom R1 ↔ B ∈ On)
113	106, 112	sylib 205	. . . . 5 ⊢ (A ∈ (R1 ‘suc B) → B ∈ On)
114	105, 113	syl5 21	. . . 4 ⊢ (¬ A ∈ (R1 ‘B) → (A ∈ (R1 ‘suc B) → B ⊆ (rank ‘A)))
115	114	imp 357	. . 3 ⊢ ((¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)) → B ⊆ (rank ‘A))
116	99	onintss 3068	. . . . . 6 ⊢ (B ∈ On → (A ∈ (R1 ‘suc B) → ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ B))
117	113, 116	mpcom 49	. . . . 5 ⊢ (A ∈ (R1 ‘suc B) → ∩{y ∈ On∣A ∈ (R1 ‘suc y)} ⊆ B)
118	117, 29	syl5ss 2156	. . . 4 ⊢ (A ∈ (R1 ‘suc B) → (rank ‘A) ⊆ B)
119	118	adantl 397	. . 3 ⊢ ((¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)) → (rank ‘A) ⊆ B)
120	115, 119	eqssd 2130	. 2 ⊢ ((¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)) → B = (rank ‘A))
121	103, 120	impbii 164	1 ⊢ (B = (rank ‘A) ↔ (¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 153   ⋀ wa 230   ⋁ w3o 786   = wceq 997   ∈ wcel 999   ≠ wne 1632  ∃wrex 1693  {crab 1695  Vcvv 1858   ⊆ wss 2098  ∅c0 2331  ∩cint 2587  ∪ciun 2620  Ord word 3004  Oncon0 3005  Lim wlim 3006  suc csuc 3007  dom cdm 3227   Fn wfn 3234   ‘cfv 3239  R₁cr1 4703  rankcrnk 4704

This theorem is referenced by:  rankr1g 4737  ssrankr1 4738  rankpw 4746

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-reg 4653  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-rab 1699  df-v 1859  df-sbc 1989  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-fv 3255  df-rdg 3990  df-r1 4705  df-rank 4706

Copyright terms: Public domain