Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem rankr1 3518

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 ∈ (R₁ ‘B) ∧ A ∈ (R₁ ‘suc B)))

**Proof of Theorem rankr1**
Step	Hyp	Ref	Expression
1		rankon 3515	. . . . 5 ⊢ (rank ‘A) ∈ On
2		eleq1 1149	. . . . 5 ⊢ (B = (rank ‘A) → (B ∈ On ↔ (rank ‘A) ∈ On))
3	1, 2	mpbiri 169	. . . 4 ⊢ (B = (rank ‘A) → B ∈ On)
4		eloni 2209	. . . . 5 ⊢ (B ∈ On → Ord B)
5		ordzsl 2366	. . . . . 6 ⊢ (Ord B ↔ (B = ∅ ∨ ∃x ∈ On B = suc x ∨ Lim B))
6		noel 1711	. . . . . . . . 9 ⊢ ¬ A ∈ ∅
7		fveq2 2832	. . . . . . . . . . 11 ⊢ (B = ∅ → (R₁ ‘B) = (R₁ ‘∅))
8		r10 3495	. . . . . . . . . . 11 ⊢ (R₁ ‘∅) = ∅
9	7, 8	syl6eq 1140	. . . . . . . . . 10 ⊢ (B = ∅ → (R₁ ‘B) = ∅)
10	9	eleq2d 1156	. . . . . . . . 9 ⊢ (B = ∅ → (A ∈ (R₁ ‘B) ↔ A ∈ ∅))
11	6, 10	mtbiri 539	. . . . . . . 8 ⊢ (B = ∅ → ¬ A ∈ (R₁ ‘B))
12	11	a1d 14	. . . . . . 7 ⊢ (B = ∅ → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B)))
13		visset 1350	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
14	13	sucid 2304	. . . . . . . . . . . . . 14 ⊢ x ∈ suc x
15		eleq2 1150	. . . . . . . . . . . . . 14 ⊢ (B = suc x → (x ∈ B ↔ x ∈ suc x))
16	14, 15	mpbiri 169	. . . . . . . . . . . . 13 ⊢ (B = suc x → x ∈ B)
17	16	adantl 305	. . . . . . . . . . . 12 ⊢ ((x ∈ On ∧ B = suc x) → x ∈ B)
18		ontri1 2232	. . . . . . . . . . . . . 14 ⊢ ((B ∈ On ∧ x ∈ On) → (B ⊆ x ↔ ¬ x ∈ B))
19	18	bicon2d 404	. . . . . . . . . . . . 13 ⊢ ((B ∈ On ∧ x ∈ On) → (x ∈ B ↔ ¬ B ⊆ x))
20		eleq1a 1158	. . . . . . . . . . . . . . 15 ⊢ (suc x ∈ On → (B = suc x → B ∈ On))
21	20	imp 277	. . . . . . . . . . . . . 14 ⊢ ((suc x ∈ On ∧ B = suc x) → B ∈ On)
22		suceloni 2314	. . . . . . . . . . . . . 14 ⊢ (x ∈ On → suc x ∈ On)
23	21, 22	sylan 343	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ∧ B = suc x) → B ∈ On)
24		pm3.26 256	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ∧ B = suc x) → x ∈ On)
25	19, 23, 24	sylanc 361	. . . . . . . . . . . 12 ⊢ ((x ∈ On ∧ B = suc x) → (x ∈ B ↔ ¬ B ⊆ x))
26	17, 25	mpbid 170	. . . . . . . . . . 11 ⊢ ((x ∈ On ∧ B = suc x) → ¬ B ⊆ x)
27	26	adantr 306	. . . . . . . . . 10 ⊢ (((x ∈ On ∧ B = suc x) ∧ B = (rank ‘A)) → ¬ B ⊆ x)
28		rankr1.1	. . . . . . . . . . . . . . . . . . 19 ⊢ A ∈ V
29	28	rankval 3512	. . . . . . . . . . . . . . . . . 18 ⊢ (rank ‘A) = ∩{y ∈ On∣A ∈ (R₁ ‘suc y)}
30	29	cleq2i 1111	. . . . . . . . . . . . . . . . 17 ⊢ (B = (rank ‘A) ↔ B = ∩{y ∈ On∣A ∈ (R₁ ‘suc y)})
31	30	biimp 133	. . . . . . . . . . . . . . . 16 ⊢ (B = (rank ‘A) → B = ∩{y ∈ On∣A ∈ (R₁ ‘suc y)})
32	31	sseq1d 1527	. . . . . . . . . . . . . . 15 ⊢ (B = (rank ‘A) → (B ⊆ x ↔ ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ x))
33		suceq 2288	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = x → suc y = suc x)
34	33	fveq2d 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (y = x → (R₁ ‘suc y) = (R₁ ‘suc x))
35	34	eleq2d 1156	. . . . . . . . . . . . . . . . 17 ⊢ (y = x → (A ∈ (R₁ ‘suc y) ↔ A ∈ (R₁ ‘suc x)))
36	35	onintss 2266	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ On → (A ∈ (R₁ ‘suc x) → ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ x))
37	36	imp 277	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On ∧ A ∈ (R₁ ‘suc x)) → ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ x)
38	32, 37	syl5bir 184	. . . . . . . . . . . . . 14 ⊢ (B = (rank ‘A) → ((x ∈ On ∧ A ∈ (R₁ ‘suc x)) → B ⊆ x))
39		fveq2 2832	. . . . . . . . . . . . . . . 16 ⊢ (B = suc x → (R₁ ‘B) = (R₁ ‘suc x))
40	39	eleq2d 1156	. . . . . . . . . . . . . . 15 ⊢ (B = suc x → (A ∈ (R₁ ‘B) ↔ A ∈ (R₁ ‘suc x)))
41	40	biimpa 324	. . . . . . . . . . . . . 14 ⊢ ((B = suc x ∧ A ∈ (R₁ ‘B)) → A ∈ (R₁ ‘suc x))
42	38, 41	sylan2i 357	. . . . . . . . . . . . 13 ⊢ (B = (rank ‘A) → ((x ∈ On ∧ (B = suc x ∧ A ∈ (R₁ ‘B))) → B ⊆ x))
43	42	exp4d 298	. . . . . . . . . . . 12 ⊢ (B = (rank ‘A) → (x ∈ On → (B = suc x → (A ∈ (R₁ ‘B) → B ⊆ x))))
44	43	com3l 34	. . . . . . . . . . 11 ⊢ (x ∈ On → (B = suc x → (B = (rank ‘A) → (A ∈ (R₁ ‘B) → B ⊆ x))))
45	44	imp31 280	. . . . . . . . . 10 ⊢ (((x ∈ On ∧ B = suc x) ∧ B = (rank ‘A)) → (A ∈ (R₁ ‘B) → B ⊆ x))
46	27, 45	mtod 95	. . . . . . . . 9 ⊢ (((x ∈ On ∧ B = suc x) ∧ B = (rank ‘A)) → ¬ A ∈ (R₁ ‘B))
47	46	exp31 293	. . . . . . . 8 ⊢ (x ∈ On → (B = suc x → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B))))
48	47	r19.23aiv 1284	. . . . . . 7 ⊢ (∃x ∈ On B = suc x → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B)))
49		eleq2 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ (B = (rank ‘A) → (x ∈ B ↔ x ∈ (rank ‘A)))
50	1	onel 2346	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ∈ (rank ‘A) → x ∈ On)
51	49, 50	syl6bi 187	. . . . . . . . . . . . . . . . . 18 ⊢ (B = (rank ‘A) → (x ∈ B → x ∈ On))
52	51	anc2li 250	. . . . . . . . . . . . . . . . 17 ⊢ (B = (rank ‘A) → (x ∈ B → (B = (rank ‘A) ∧ x ∈ On)))
53		r1ord2 3500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc x ∈ On → (x ∈ suc x → (R₁ ‘x) ⊆ (R₁ ‘suc x)))
54	14, 53	mpi 44	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
55	22, 54	syl 12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
56	55	sseld 1506	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ∈ On → (A ∈ (R₁ ‘x) → A ∈ (R₁ ‘suc x)))
57	29	sseq1i 1524	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((rank ‘A) ⊆ x ↔ ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ x)
58	36, 57	syl6ibr 186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ∈ On → (A ∈ (R₁ ‘suc x) → (rank ‘A) ⊆ x))
59	56, 58	syld 27	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ∈ On → (A ∈ (R₁ ‘x) → (rank ‘A) ⊆ x))
60		sseq1 1521	. . . . . . . . . . . . . . . . . . . 20 ⊢ (B = (rank ‘A) → (B ⊆ x ↔ (rank ‘A) ⊆ x))
61	60	biimprd 136	. . . . . . . . . . . . . . . . . . 19 ⊢ (B = (rank ‘A) → ((rank ‘A) ⊆ x → B ⊆ x))
62	59, 61	sylan9r 360	. . . . . . . . . . . . . . . . . 18 ⊢ ((B = (rank ‘A) ∧ x ∈ On) → (A ∈ (R₁ ‘x) → B ⊆ x))
63	18, 3	sylan 343	. . . . . . . . . . . . . . . . . 18 ⊢ ((B = (rank ‘A) ∧ x ∈ On) → (B ⊆ x ↔ ¬ x ∈ B))
64	62, 63	sylibd 177	. . . . . . . . . . . . . . . . 17 ⊢ ((B = (rank ‘A) ∧ x ∈ On) → (A ∈ (R₁ ‘x) → ¬ x ∈ B))
65	52, 64	syl6 23	. . . . . . . . . . . . . . . 16 ⊢ (B = (rank ‘A) → (x ∈ B → (A ∈ (R₁ ‘x) → ¬ x ∈ B)))
66	65	com3l 34	. . . . . . . . . . . . . . 15 ⊢ (x ∈ B → (A ∈ (R₁ ‘x) → (B = (rank ‘A) → ¬ x ∈ B)))
67		con2 82	. . . . . . . . . . . . . . 15 ⊢ ((B = (rank ‘A) → ¬ x ∈ B) → (x ∈ B → ¬ B = (rank ‘A)))
68	66, 67	syl6 23	. . . . . . . . . . . . . 14 ⊢ (x ∈ B → (A ∈ (R₁ ‘x) → (x ∈ B → ¬ B = (rank ‘A))))
69	68	pm2.43a 60	. . . . . . . . . . . . 13 ⊢ (x ∈ B → (A ∈ (R₁ ‘x) → ¬ B = (rank ‘A)))
70	69	r19.23aiv 1284	. . . . . . . . . . . 12 ⊢ (∃x ∈ B A ∈ (R₁ ‘x) → ¬ B = (rank ‘A))
71	70	con2i 89	. . . . . . . . . . 11 ⊢ (B = (rank ‘A) → ¬ ∃x ∈ B A ∈ (R₁ ‘x))
72	71	adantr 306	. . . . . . . . . 10 ⊢ ((B = (rank ‘A) ∧ Lim B) → ¬ ∃x ∈ B A ∈ (R₁ ‘x))
73		r1lim 3497	. . . . . . . . . . . . 13 ⊢ ((B ∈ V ∧ Lim B) → (R₁ ‘B) = ∪x ∈ B (R₁ ‘x))
74		fvex 2838	. . . . . . . . . . . . . 14 ⊢ (rank ‘A) ∈ V
75		eleq1 1149	. . . . . . . . . . . . . 14 ⊢ (B = (rank ‘A) → (B ∈ V ↔ (rank ‘A) ∈ V))
76	74, 75	mpbiri 169	. . . . . . . . . . . . 13 ⊢ (B = (rank ‘A) → B ∈ V)
77	73, 76	sylan 343	. . . . . . . . . . . 12 ⊢ ((B = (rank ‘A) ∧ Lim B) → (R₁ ‘B) = ∪x ∈ B (R₁ ‘x))
78	77	eleq2d 1156	. . . . . . . . . . 11 ⊢ ((B = (rank ‘A) ∧ Lim B) → (A ∈ (R₁ ‘B) ↔ A ∈ ∪x ∈ B (R₁ ‘x)))
79		eliun 1998	. . . . . . . . . . 11 ⊢ (A ∈ ∪x ∈ B (R₁ ‘x) ↔ ∃x ∈ B A ∈ (R₁ ‘x))
80	78, 79	syl6bb 414	. . . . . . . . . 10 ⊢ ((B = (rank ‘A) ∧ Lim B) → (A ∈ (R₁ ‘B) ↔ ∃x ∈ B A ∈ (R₁ ‘x)))
81	72, 80	mtbird 537	. . . . . . . . 9 ⊢ ((B = (rank ‘A) ∧ Lim B) → ¬ A ∈ (R₁ ‘B))
82	81	exp 291	. . . . . . . 8 ⊢ (B = (rank ‘A) → (Lim B → ¬ A ∈ (R₁ ‘B)))
83	82	com12 13	. . . . . . 7 ⊢ (Lim B → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B)))
84	12, 48, 83	3jaoi 633	. . . . . 6 ⊢ ((B = ∅ ∨ ∃x ∈ On B = suc x ∨ Lim B) → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B)))
85	5, 84	sylbi 174	. . . . 5 ⊢ (Ord B → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B)))
86	4, 85	syl 12	. . . 4 ⊢ (B ∈ On → (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B)))
87	3, 86	mpcom 49	. . 3 ⊢ (B = (rank ‘A) → ¬ A ∈ (R₁ ‘B))
88		ssrab 1556	. . . . . . 7 ⊢ {y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ On
89		rankwflem 3509	. . . . . . . . 9 ⊢ (A ∈ V → ∃y ∈ On A ∈ (R₁ ‘suc y))
90	28, 89	ax-mp 6	. . . . . . . 8 ⊢ ∃y ∈ On A ∈ (R₁ ‘suc y)
91		rabn0 1716	. . . . . . . 8 ⊢ (¬ {y ∈ On∣A ∈ (R₁ ‘suc y)} = ∅ ↔ ∃y ∈ On A ∈ (R₁ ‘suc y))
92	90, 91	mpbir 165	. . . . . . 7 ⊢ ¬ {y ∈ On∣A ∈ (R₁ ‘suc y)} = ∅
93		onint 2261	. . . . . . 7 ⊢ (({y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ On ∧ ¬ {y ∈ On∣A ∈ (R₁ ‘suc y)} = ∅) → ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)})
94	88, 92, 93	mp2an 520	. . . . . 6 ⊢ ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)}
95	29, 94	eqeltr 1159	. . . . 5 ⊢ (rank ‘A) ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)}
96		eleq1 1149	. . . . 5 ⊢ (B = (rank ‘A) → (B ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)} ↔ (rank ‘A) ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)}))
97	95, 96	mpbiri 169	. . . 4 ⊢ (B = (rank ‘A) → B ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)})
98		suceq 2288	. . . . . . . 8 ⊢ (y = B → suc y = suc B)
99	98	fveq2d 2836	. . . . . . 7 ⊢ (y = B → (R₁ ‘suc y) = (R₁ ‘suc B))
100	99	eleq2d 1156	. . . . . 6 ⊢ (y = B → (A ∈ (R₁ ‘suc y) ↔ A ∈ (R₁ ‘suc B)))
101	100	elrab 1422	. . . . 5 ⊢ (B ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)} ↔ (B ∈ On ∧ A ∈ (R₁ ‘suc B)))
102	101	pm3.27bd 263	. . . 4 ⊢ (B ∈ {y ∈ On∣A ∈ (R₁ ‘suc y)} → A ∈ (R₁ ‘suc B))
103	97, 102	syl 12	. . 3 ⊢ (B = (rank ‘A) → A ∈ (R₁ ‘suc B))
104	87, 103	jca 236	. 2 ⊢ (B = (rank ‘A) → (¬ A ∈ (R₁ ‘B) ∧ A ∈ (R₁ ‘suc B)))
105	28	rankr1lem 3517	. . . . . 6 ⊢ (B ∈ On → (¬ A ∈ (R₁ ‘B) → B ⊆ (rank ‘A)))
106	105	com12 13	. . . . 5 ⊢ (¬ A ∈ (R₁ ‘B) → (B ∈ On → B ⊆ (rank ‘A)))
107		ndmfv 2848	. . . . . . . . 9 ⊢ (¬ suc B ∈ dom R₁ → (R₁ ‘suc B) = ∅)
108	107	eleq2d 1156	. . . . . . . 8 ⊢ (¬ suc B ∈ dom R₁ → (A ∈ (R₁ ‘suc B) ↔ A ∈ ∅))
109	6, 108	mtbiri 539	. . . . . . 7 ⊢ (¬ suc B ∈ dom R₁ → ¬ A ∈ (R₁ ‘suc B))
110	109	a3i 69	. . . . . 6 ⊢ (A ∈ (R₁ ‘suc B) → suc B ∈ dom R₁)
111		r1fnon 3494	. . . . . . . . 9 ⊢ R₁ Fn On
112		fndm 2723	. . . . . . . . 9 ⊢ (R₁ Fn On → dom R₁ = On)
113	111, 112	ax-mp 6	. . . . . . . 8 ⊢ dom R₁ = On
114	113	eleq2i 1153	. . . . . . 7 ⊢ (suc B ∈ dom R₁ ↔ suc B ∈ On)
115		sucelon 2319	. . . . . . 7 ⊢ (B ∈ On ↔ suc B ∈ On)
116	114, 115	bitr4 154	. . . . . 6 ⊢ (suc B ∈ dom R₁ ↔ B ∈ On)
117	110, 116	sylib 173	. . . . 5 ⊢ (A ∈ (R₁ ‘suc B) → B ∈ On)
118	106, 117	syl5 22	. . . 4 ⊢ (¬ A ∈ (R₁ ‘B) → (A ∈ (R₁ ‘suc B) → B ⊆ (rank ‘A)))
119	118	imp 277	. . 3 ⊢ ((¬ A ∈ (R₁ ‘B) ∧ A ∈ (R₁ ‘suc B)) → B ⊆ (rank ‘A))
120	100	onintss 2266	. . . . . 6 ⊢ (B ∈ On → (A ∈ (R₁ ‘suc B) → ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ B))
121	117, 120	mpcom 49	. . . . 5 ⊢ (A ∈ (R₁ ‘suc B) → ∩{y ∈ On∣A ∈ (R₁ ‘suc y)} ⊆ B)
122	121, 29	syl5ss 1544	. . . 4 ⊢ (A ∈ (R₁ ‘suc B) → (rank ‘A) ⊆ B)
123	122	adantl 305	. . 3 ⊢ ((¬ A ∈ (R₁ ‘B) ∧ A ∈ (R₁ ‘suc B)) → (rank ‘A) ⊆ B)
124	119, 123	eqssd 1518	. 2 ⊢ ((¬ A ∈ (R₁ ‘B) ∧ A ∈ (R₁ ‘suc B)) → B = (rank ‘A))
125	104, 124	impbi 139	1 ⊢ (B = (rank ‘A) ↔ (¬ A ∈ (R₁ ‘B) ∧ A ∈ (R₁ ‘suc B)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∨ w3o 580 = weq 797 = wceq 1091 ∈ wcel 1092 ∃wrex 1202 {crab 1204 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 ∩cint 1965 ∪ciun 1994 Ord word 2198 Oncon0 2199 Lim wlim 2200 suc csuc 2201 dom cdm 2410 Fn wfn 2417 ‘cfv 2422 R₁cr1 3485 rankcrnk 3486

This theorem is referenced by: rankr1g 3519 ssrankr1 3520 rankpw 3528

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-r1 3487 df-rank 3488

metamath.org