Theorem rankcf 9914

Description: Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of 𝐴 form a cofinal map into (rank‘𝐴). (Contributed by Mario Carneiro, 27-May-2013.)

Assertion

Ref	Expression
rankcf	⊢ ¬ 𝐴 ≺ (cf‘(rank‘𝐴))

Proof of Theorem rankcf

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rankon 8935	. . 3 ⊢ (rank‘𝐴) ∈ On
2		onzsl 7307	. . 3 ⊢ ((rank‘𝐴) ∈ On ↔ ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))))
3	1, 2	mpbi 222	. 2 ⊢ ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)))
4		sdom0 8361	. . . 4 ⊢ ¬ 𝐴 ≺ ∅
5		fveq2 6433	. . . . . 6 ⊢ ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = (cf‘∅))
6		cf0 9388	. . . . . 6 ⊢ (cf‘∅) = ∅
7	5, 6	syl6eq 2877	. . . . 5 ⊢ ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = ∅)
8	7	breq2d 4885	. . . 4 ⊢ ((rank‘𝐴) = ∅ → (𝐴 ≺ (cf‘(rank‘𝐴)) ↔ 𝐴 ≺ ∅))
9	4, 8	mtbiri 319	. . 3 ⊢ ((rank‘𝐴) = ∅ → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
10		fveq2 6433	. . . . . . 7 ⊢ ((rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) = (cf‘suc 𝑥))
11		cfsuc 9394	. . . . . . 7 ⊢ (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
12	10, 11	sylan9eqr 2883	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) = 1o)
13		nsuceq0 6043	. . . . . . . . 9 ⊢ suc 𝑥 ≠ ∅
14		neeq1 3061	. . . . . . . . 9 ⊢ ((rank‘𝐴) = suc 𝑥 → ((rank‘𝐴) ≠ ∅ ↔ suc 𝑥 ≠ ∅))
15	13, 14	mpbiri 250	. . . . . . . 8 ⊢ ((rank‘𝐴) = suc 𝑥 → (rank‘𝐴) ≠ ∅)
16		fveq2 6433	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → (rank‘𝐴) = (rank‘∅))
17		0elon 6016	. . . . . . . . . . . . 13 ⊢ ∅ ∈ On
18		r1fnon 8907	. . . . . . . . . . . . . 14 ⊢ 𝑅1 Fn On
19		fndm 6223	. . . . . . . . . . . . . 14 ⊢ (𝑅1 Fn On → dom 𝑅1 = On)
20	18, 19	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom 𝑅1 = On
21	17, 20	eleqtrri 2905	. . . . . . . . . . . 12 ⊢ ∅ ∈ dom 𝑅1
22		rankonid 8969	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝑅1 ↔ (rank‘∅) = ∅)
23	21, 22	mpbi 222	. . . . . . . . . . 11 ⊢ (rank‘∅) = ∅
24	16, 23	syl6eq 2877	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (rank‘𝐴) = ∅)
25	24	necon3i 3031	. . . . . . . . 9 ⊢ ((rank‘𝐴) ≠ ∅ → 𝐴 ≠ ∅)
26		rankvaln 8939	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅)
27	26	necon1ai 3026	. . . . . . . . . 10 ⊢ ((rank‘𝐴) ≠ ∅ → 𝐴 ∈ ∪ (𝑅1 “ On))
28		breq2 4877	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → (1o ≼ 𝑦 ↔ 1o ≼ 𝐴))
29		neeq1 3061	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → (𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅))
30		0sdom1dom 8427	. . . . . . . . . . . 12 ⊢ (∅ ≺ 𝑦 ↔ 1o ≼ 𝑦)
31		vex 3417	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
32	31	0sdom 8360	. . . . . . . . . . . 12 ⊢ (∅ ≺ 𝑦 ↔ 𝑦 ≠ ∅)
33	30, 32	bitr3i 269	. . . . . . . . . . 11 ⊢ (1o ≼ 𝑦 ↔ 𝑦 ≠ ∅)
34	28, 29, 33	vtoclbg 3483	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (1o ≼ 𝐴 ↔ 𝐴 ≠ ∅))
35	27, 34	syl 17	. . . . . . . . 9 ⊢ ((rank‘𝐴) ≠ ∅ → (1o ≼ 𝐴 ↔ 𝐴 ≠ ∅))
36	25, 35	mpbird 249	. . . . . . . 8 ⊢ ((rank‘𝐴) ≠ ∅ → 1o ≼ 𝐴)
37	15, 36	syl 17	. . . . . . 7 ⊢ ((rank‘𝐴) = suc 𝑥 → 1o ≼ 𝐴)
38	37	adantl 475	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → 1o ≼ 𝐴)
39	12, 38	eqbrtrd 4895	. . . . 5 ⊢ ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) ≼ 𝐴)
40	39	rexlimiva 3237	. . . 4 ⊢ (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) ≼ 𝐴)
41		domnsym 8355	. . . 4 ⊢ ((cf‘(rank‘𝐴)) ≼ 𝐴 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
42	40, 41	syl 17	. . 3 ⊢ (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
43		nlim0 6021	. . . . . . . . . . . . . . . . 17 ⊢ ¬ Lim ∅
44		limeq 5975	. . . . . . . . . . . . . . . . 17 ⊢ ((rank‘𝐴) = ∅ → (Lim (rank‘𝐴) ↔ Lim ∅))
45	43, 44	mtbiri 319	. . . . . . . . . . . . . . . 16 ⊢ ((rank‘𝐴) = ∅ → ¬ Lim (rank‘𝐴))
46	26, 45	syl 17	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → ¬ Lim (rank‘𝐴))
47	46	con4i 114	. . . . . . . . . . . . . 14 ⊢ (Lim (rank‘𝐴) → 𝐴 ∈ ∪ (𝑅1 “ On))
48		r1elssi 8945	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On))
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (Lim (rank‘𝐴) → 𝐴 ⊆ ∪ (𝑅1 “ On))
50	49	sselda 3827	. . . . . . . . . . . 12 ⊢ ((Lim (rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ (𝑅1 “ On))
51		ranksnb 8967	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → (rank‘{𝑥}) = suc (rank‘𝑥))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ ((Lim (rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → (rank‘{𝑥}) = suc (rank‘𝑥))
53		rankelb 8964	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
54	47, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (Lim (rank‘𝐴) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
55		limsuc 7310	. . . . . . . . . . . . 13 ⊢ (Lim (rank‘𝐴) → ((rank‘𝑥) ∈ (rank‘𝐴) ↔ suc (rank‘𝑥) ∈ (rank‘𝐴)))
56	54, 55	sylibd 231	. . . . . . . . . . . 12 ⊢ (Lim (rank‘𝐴) → (𝑥 ∈ 𝐴 → suc (rank‘𝑥) ∈ (rank‘𝐴)))
57	56	imp 397	. . . . . . . . . . 11 ⊢ ((Lim (rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → suc (rank‘𝑥) ∈ (rank‘𝐴))
58	52, 57	eqeltrd 2906	. . . . . . . . . 10 ⊢ ((Lim (rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → (rank‘{𝑥}) ∈ (rank‘𝐴))
59		eleq1a 2901	. . . . . . . . . 10 ⊢ ((rank‘{𝑥}) ∈ (rank‘𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
60	58, 59	syl 17	. . . . . . . . 9 ⊢ ((Lim (rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
61	60	rexlimdva 3240	. . . . . . . 8 ⊢ (Lim (rank‘𝐴) → (∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
62	61	abssdv 3901	. . . . . . 7 ⊢ (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴))
63		snex 5129	. . . . . . . . . . . . 13 ⊢ {𝑥} ∈ V
64	63	dfiun2 4774	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}
65		iunid 4795	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴
66	64, 65	eqtr3i 2851	. . . . . . . . . . 11 ⊢ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} = 𝐴
67	66	fveq2i 6436	. . . . . . . . . 10 ⊢ (rank‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}) = (rank‘𝐴)
68	48	sselda 3827	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ (𝑅1 “ On))
69		snwf 8949	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → {𝑥} ∈ ∪ (𝑅1 “ On))
70		eleq1a 2901	. . . . . . . . . . . . . . 15 ⊢ ({𝑥} ∈ ∪ (𝑅1 “ On) → (𝑦 = {𝑥} → 𝑦 ∈ ∪ (𝑅1 “ On)))
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ 𝐴) → (𝑦 = {𝑥} → 𝑦 ∈ ∪ (𝑅1 “ On)))
72	71	rexlimdva 3240	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (∃𝑥 ∈ 𝐴 𝑦 = {𝑥} → 𝑦 ∈ ∪ (𝑅1 “ On)))
73	72	abssdv 3901	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪ (𝑅1 “ On))
74		abrexexg 7402	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ V)
75		eleq1 2894	. . . . . . . . . . . . . 14 ⊢ (𝑧 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} → (𝑧 ∈ ∪ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪ (𝑅1 “ On)))
76		sseq1 3851	. . . . . . . . . . . . . 14 ⊢ (𝑧 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} → (𝑧 ⊆ ∪ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪ (𝑅1 “ On)))
77		vex 3417	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
78	77	r1elss 8946	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) ↔ 𝑧 ⊆ ∪ (𝑅1 “ On))
79	75, 76, 78	vtoclbg 3483	. . . . . . . . . . . . 13 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ V → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪ (𝑅1 “ On)))
80	74, 79	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪ (𝑅1 “ On)))
81	73, 80	mpbird 249	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪ (𝑅1 “ On))
82		rankuni2b 8993	. . . . . . . . . . 11 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪ (𝑅1 “ On) → (rank‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}) = ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧))
83	81, 82	syl 17	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}) = ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧))
84	67, 83	syl5eqr 2875	. . . . . . . . 9 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧))
85		fvex 6446	. . . . . . . . . . 11 ⊢ (rank‘𝑧) ∈ V
86	85	dfiun2 4774	. . . . . . . . . 10 ⊢ ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧) = ∪ {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)}
87		fveq2 6433	. . . . . . . . . . . 12 ⊢ (𝑧 = {𝑥} → (rank‘𝑧) = (rank‘{𝑥}))
88	63, 87	abrexco 6757	. . . . . . . . . . 11 ⊢ {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})}
89	88	unieqi 4667	. . . . . . . . . 10 ⊢ ∪ {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})}
90	86, 89	eqtri 2849	. . . . . . . . 9 ⊢ ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧) = ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})}
91	84, 90	syl6req 2878	. . . . . . . 8 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
92	47, 91	syl 17	. . . . . . 7 ⊢ (Lim (rank‘𝐴) → ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
93		fvex 6446	. . . . . . . 8 ⊢ (rank‘𝐴) ∈ V
94	93	cfslb 9403	. . . . . . 7 ⊢ ((Lim (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴) ∧ ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})})
95	62, 92, 94	mpd3an23 1593	. . . . . 6 ⊢ (Lim (rank‘𝐴) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})})
96		2fveq3 6438	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴)))
97		breq12 4878	. . . . . . . . . 10 ⊢ ((𝑦 = 𝐴 ∧ (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴))) → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
98	96, 97	mpdan 680	. . . . . . . . 9 ⊢ (𝑦 = 𝐴 → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
99		rexeq 3351	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥}) ↔ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})))
100	99	abbidv 2946	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})})
101		breq12 4878	. . . . . . . . . 10 ⊢ (({𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ∧ 𝑦 = 𝐴) → ({𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
102	100, 101	mpancom 681	. . . . . . . . 9 ⊢ (𝑦 = 𝐴 → ({𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
103	98, 102	imbi12d 336	. . . . . . . 8 ⊢ (𝑦 = 𝐴 → ((𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦) ↔ (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)))
104		eqid 2825	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) = (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥}))
105	104	rnmpt 5604	. . . . . . . . 9 ⊢ ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) = {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})}
106		cfon 9392	. . . . . . . . . . 11 ⊢ (cf‘(rank‘𝑦)) ∈ On
107		sdomdom 8250	. . . . . . . . . . 11 ⊢ (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ≼ (cf‘(rank‘𝑦)))
108		ondomen 9173	. . . . . . . . . . 11 ⊢ (((cf‘(rank‘𝑦)) ∈ On ∧ 𝑦 ≼ (cf‘(rank‘𝑦))) → 𝑦 ∈ dom card)
109	106, 107, 108	sylancr 583	. . . . . . . . . 10 ⊢ (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ∈ dom card)
110		fvex 6446	. . . . . . . . . . . 12 ⊢ (rank‘{𝑥}) ∈ V
111	110, 104	fnmpti 6255	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) Fn 𝑦
112		dffn4 6359	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) Fn 𝑦 ↔ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})):𝑦–onto→ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})))
113	111, 112	mpbi 222	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})):𝑦–onto→ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥}))
114		fodomnum 9193	. . . . . . . . . 10 ⊢ (𝑦 ∈ dom card → ((𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})):𝑦–onto→ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) → ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦))
115	109, 113, 114	mpisyl 21	. . . . . . . . 9 ⊢ (𝑦 ≺ (cf‘(rank‘𝑦)) → ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦)
116	105, 115	syl5eqbrr 4909	. . . . . . . 8 ⊢ (𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦)
117	103, 116	vtoclg 3482	. . . . . . 7 ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
118	47, 117	syl 17	. . . . . 6 ⊢ (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
119		domtr 8275	. . . . . . 7 ⊢ (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → (cf‘(rank‘𝐴)) ≼ 𝐴)
120	119, 41	syl 17	. . . . . 6 ⊢ (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
121	95, 118, 120	syl6an 676	. . . . 5 ⊢ (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))))
122	121	pm2.01d 182	. . . 4 ⊢ (Lim (rank‘𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
123	122	adantl 475	. . 3 ⊢ (((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
124	9, 42, 123	3jaoi 1558	. 2 ⊢ (((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
125	3, 124	ax-mp 5	1 ⊢ ¬ 𝐴 ≺ (cf‘(rank‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ w3o 1112   = wceq 1658   ∈ wcel 2166  {cab 2811   ≠ wne 2999  ∃wrex 3118  Vcvv 3414   ⊆ wss 3798  ∅c0 4144  {csn 4397  ∪ cuni 4658  ∪ ciun 4740   class class class wbr 4873   ↦ cmpt 4952  dom cdm 5342  ran crn 5343   “ cima 5345  Oncon0 5963  Lim wlim 5964  suc csuc 5965   Fn wfn 6118  –onto→wfo 6121  ‘cfv 6123  1_oc1o 7819   ≼ cdom 8220   ≺ csdm 8221  𝑅₁cr1 8902  rankcrnk 8903  cardccrd 9074  cfccf 9076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-r1 8904  df-rank 8905  df-card 9078  df-cf 9080  df-acn 9081

This theorem is referenced by:  inatsk  9915  grur1  9957