Theorem grur1 10839

Description: A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.)

Hypothesis

Ref	Expression
gruina.1	⊢ 𝐴 = (𝑈 ∩ On)

Assertion

Ref	Expression
grur1	⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴))

Proof of Theorem grur1

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

Step	Hyp	Ref	Expression
1		nss 4028	. . . . 5 ⊢ (¬ 𝑈 ⊆ (𝑅1‘𝐴) ↔ ∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴)))
2		fveqeq2 6890	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((rank‘𝑦) = 𝐴 ↔ (rank‘𝑥) = 𝐴))
3	2	rspcev 3606	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑈 ∧ (rank‘𝑥) = 𝐴) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)
4	3	ex 412	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑈 → ((rank‘𝑥) = 𝐴 → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
5	4	ad2antrl 728	. . . . . . . 8 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ((rank‘𝑥) = 𝐴 → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
6		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑈 ∈ ∪ (𝑅1 “ On))
7		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑥 ∈ 𝑈)
8		r1elssi 9824	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ ∪ (𝑅1 “ On) → 𝑈 ⊆ ∪ (𝑅1 “ On))
9	8	sseld 3962	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝑈 → 𝑥 ∈ ∪ (𝑅1 “ On)))
10	6, 7, 9	sylc 65	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑥 ∈ ∪ (𝑅1 “ On))
11		tcrank 9903	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → (rank‘𝑥) = (rank “ (TC‘𝑥)))
12	10, 11	syl 17	. . . . . . . . . 10 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (rank‘𝑥) = (rank “ (TC‘𝑥)))
13	12	eleq2d 2821	. . . . . . . . 9 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank‘𝑥) ↔ 𝐴 ∈ (rank “ (TC‘𝑥))))
14		gruelss 10813	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝑥 ⊆ 𝑈)
15		grutr 10812	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ Univ → Tr 𝑈)
16	15	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → Tr 𝑈)
17		vex 3468	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
18		tcmin 9760	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ V → ((𝑥 ⊆ 𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈))
19	17, 18	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ 𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈)
20	14, 16, 19	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (TC‘𝑥) ⊆ 𝑈)
21		rankf 9813	. . . . . . . . . . . . 13 ⊢ rank:∪ (𝑅1 “ On)⟶On
22		ffun 6714	. . . . . . . . . . . . 13 ⊢ (rank:∪ (𝑅1 “ On)⟶On → Fun rank)
23	21, 22	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun rank
24		fvelima 6949	. . . . . . . . . . . 12 ⊢ ((Fun rank ∧ 𝐴 ∈ (rank “ (TC‘𝑥))) → ∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴)
25	23, 24	mpan 690	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴)
26		ssrexv 4033	. . . . . . . . . . 11 ⊢ ((TC‘𝑥) ⊆ 𝑈 → (∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴 → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
27	20, 25, 26	syl2im 40	. . . . . . . . . 10 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
28	27	ad2ant2r 747	. . . . . . . . 9 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
29	13, 28	sylbid 240	. . . . . . . 8 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank‘𝑥) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
30		simprr 772	. . . . . . . . . 10 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ¬ 𝑥 ∈ (𝑅1‘𝐴))
31		ne0i 4321	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑈 → 𝑈 ≠ ∅)
32		gruina.1	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 = (𝑈 ∩ On)
33	32	gruina 10837	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
34	31, 33	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ Inacc)
35		inawina 10709	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
36		winaon 10707	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
37	34, 35, 36	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ On)
38		r1fnon 9786	. . . . . . . . . . . . . 14 ⊢ 𝑅1 Fn On
39		fndm 6646	. . . . . . . . . . . . . 14 ⊢ (𝑅1 Fn On → dom 𝑅1 = On)
40	38, 39	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom 𝑅1 = On
41	37, 40	eleqtrrdi 2846	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ dom 𝑅1)
42	41	ad2ant2r 747	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝐴 ∈ dom 𝑅1)
43		rankr1ag 9821	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) → (𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
44	10, 42, 43	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
45	30, 44	mtbid 324	. . . . . . . . 9 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ¬ (rank‘𝑥) ∈ 𝐴)
46		rankon 9814	. . . . . . . . . . . . 13 ⊢ (rank‘𝑥) ∈ On
47		eloni 6367	. . . . . . . . . . . . . 14 ⊢ ((rank‘𝑥) ∈ On → Ord (rank‘𝑥))
48		eloni 6367	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → Ord 𝐴)
49		ordtri3or 6389	. . . . . . . . . . . . . 14 ⊢ ((Ord (rank‘𝑥) ∧ Ord 𝐴) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))
50	47, 48, 49	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((rank‘𝑥) ∈ On ∧ 𝐴 ∈ On) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))
51	46, 37, 50	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))
52		3orass 1089	. . . . . . . . . . . 12 ⊢ (((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)) ↔ ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))))
53	51, 52	sylib 218	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))))
54	53	ord 864	. . . . . . . . . 10 ⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))))
55	54	ad2ant2r 747	. . . . . . . . 9 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))))
56	45, 55	mpd 15	. . . . . . . 8 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))
57	5, 29, 56	mpjaod 860	. . . . . . 7 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)
58	57	ex 412	. . . . . 6 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → ((𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
59	58	exlimdv 1933	. . . . 5 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
60	1, 59	biimtrid 242	. . . 4 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (¬ 𝑈 ⊆ (𝑅1‘𝐴) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴))
61		simpll 766	. . . . . . 7 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ∈ Univ)
62		ne0i 4321	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑈 → 𝑈 ≠ ∅)
63	62, 33	sylan2 593	. . . . . . . . 9 ⊢ ((𝑈 ∈ Univ ∧ 𝑦 ∈ 𝑈) → 𝐴 ∈ Inacc)
64	63	ad2ant2r 747	. . . . . . . 8 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ Inacc)
65	64, 35, 36	3syl 18	. . . . . . 7 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ On)
66		simprl 770	. . . . . . 7 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑦 ∈ 𝑈)
67		fveq2 6881	. . . . . . . . . 10 ⊢ ((rank‘𝑦) = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘𝐴))
68	67	ad2antll 729	. . . . . . . . 9 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = (cf‘𝐴))
69		elina 10706	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴))
70	69	simp2bi 1146	. . . . . . . . . 10 ⊢ (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
71	64, 70	syl 17	. . . . . . . . 9 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘𝐴) = 𝐴)
72	68, 71	eqtrd 2771	. . . . . . . 8 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = 𝐴)
73		rankcf 10796	. . . . . . . . 9 ⊢ ¬ 𝑦 ≺ (cf‘(rank‘𝑦))
74		fvex 6894	. . . . . . . . . 10 ⊢ (cf‘(rank‘𝑦)) ∈ V
75		vex 3468	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
76		domtri 10575	. . . . . . . . . 10 ⊢ (((cf‘(rank‘𝑦)) ∈ V ∧ 𝑦 ∈ V) → ((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦))))
77	74, 75, 76	mp2an 692	. . . . . . . . 9 ⊢ ((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦)))
78	73, 77	mpbir 231	. . . . . . . 8 ⊢ (cf‘(rank‘𝑦)) ≼ 𝑦
79	72, 78	eqbrtrrdi 5164	. . . . . . 7 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ≼ 𝑦)
80		grudomon 10836	. . . . . . 7 ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝑦 ∈ 𝑈 ∧ 𝐴 ≼ 𝑦)) → 𝐴 ∈ 𝑈)
81	61, 65, 66, 79, 80	syl112anc 1376	. . . . . 6 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ 𝑈)
82		elin 3947	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On))
83	82	biimpri 228	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On))
84	83, 32	eleqtrrdi 2846	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ 𝐴)
85		ordirr 6375	. . . . . . . . 9 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
86	48, 85	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴)
87	86	adantl 481	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → ¬ 𝐴 ∈ 𝐴)
88	84, 87	pm2.21dd 195	. . . . . 6 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝑈 ⊆ (𝑅1‘𝐴))
89	81, 65, 88	syl2anc 584	. . . . 5 ⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ⊆ (𝑅1‘𝐴))
90	89	rexlimdvaa 3143	. . . 4 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴 → 𝑈 ⊆ (𝑅1‘𝐴)))
91	60, 90	syld 47	. . 3 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (¬ 𝑈 ⊆ (𝑅1‘𝐴) → 𝑈 ⊆ (𝑅1‘𝐴)))
92	91	pm2.18d 127	. 2 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 ⊆ (𝑅1‘𝐴))
93	32	grur1a 10838	. . 3 ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈)
94	93	adantr 480	. 2 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (𝑅1‘𝐴) ⊆ 𝑈)
95	92, 94	eqssd 3981	1 ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  Vcvv 3464   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  ∪ cuni 4888   class class class wbr 5124  Tr wtr 5234  dom cdm 5659   “ cima 5662  Ord word 6356  Oncon0 6357  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536   ≼ cdom 8962   ≺ csdm 8963  TCctc 9755  𝑅₁cr1 9781  rankcrnk 9782  cfccf 9956  Inacc_wcwina 10701  Inacccina 10702  Univcgru 10809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-inf2 9660  ax-ac2 10482

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-tc 9756  df-r1 9783  df-rank 9784  df-card 9958  df-cf 9960  df-acn 9961  df-ac 10135  df-wina 10703  df-ina 10704  df-gru 10810

This theorem is referenced by:  grutsk  10841  bj-grur1  37086  grurankcld  44232