MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grur1 Structured version   Visualization version   GIF version

Theorem grur1 9593
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.
StepHypRef Expression
1 nss 3647 . . . . 5 𝑈 ⊆ (𝑅1𝐴) ↔ ∃𝑥(𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴)))
2 fveq2 6153 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (rank‘𝑦) = (rank‘𝑥))
32eqeq1d 2623 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((rank‘𝑦) = 𝐴 ↔ (rank‘𝑥) = 𝐴))
43rspcev 3298 . . . . . . . . . 10 ((𝑥𝑈 ∧ (rank‘𝑥) = 𝐴) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴)
54ex 450 . . . . . . . . 9 (𝑥𝑈 → ((rank‘𝑥) = 𝐴 → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
65ad2antrl 763 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ((rank‘𝑥) = 𝐴 → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
7 simplr 791 . . . . . . . . . . . 12 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝑈 (𝑅1 “ On))
8 simprl 793 . . . . . . . . . . . 12 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝑥𝑈)
9 r1elssi 8619 . . . . . . . . . . . . 13 (𝑈 (𝑅1 “ On) → 𝑈 (𝑅1 “ On))
109sseld 3586 . . . . . . . . . . . 12 (𝑈 (𝑅1 “ On) → (𝑥𝑈𝑥 (𝑅1 “ On)))
117, 8, 10sylc 65 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝑥 (𝑅1 “ On))
12 tcrank 8698 . . . . . . . . . . 11 (𝑥 (𝑅1 “ On) → (rank‘𝑥) = (rank “ (TC‘𝑥)))
1311, 12syl 17 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (rank‘𝑥) = (rank “ (TC‘𝑥)))
1413eleq2d 2684 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝐴 ∈ (rank‘𝑥) ↔ 𝐴 ∈ (rank “ (TC‘𝑥))))
15 gruelss 9567 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝑥𝑈)
16 grutr 9566 . . . . . . . . . . . . 13 (𝑈 ∈ Univ → Tr 𝑈)
1716adantr 481 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → Tr 𝑈)
18 vex 3192 . . . . . . . . . . . . 13 𝑥 ∈ V
19 tcmin 8568 . . . . . . . . . . . . 13 (𝑥 ∈ V → ((𝑥𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈))
2018, 19ax-mp 5 . . . . . . . . . . . 12 ((𝑥𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈)
2115, 17, 20syl2anc 692 . . . . . . . . . . 11 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (TC‘𝑥) ⊆ 𝑈)
22 rankf 8608 . . . . . . . . . . . . 13 rank: (𝑅1 “ On)⟶On
23 ffun 6010 . . . . . . . . . . . . 13 (rank: (𝑅1 “ On)⟶On → Fun rank)
2422, 23ax-mp 5 . . . . . . . . . . . 12 Fun rank
25 fvelima 6210 . . . . . . . . . . . 12 ((Fun rank ∧ 𝐴 ∈ (rank “ (TC‘𝑥))) → ∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴)
2624, 25mpan 705 . . . . . . . . . . 11 (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴)
27 ssrexv 3651 . . . . . . . . . . 11 ((TC‘𝑥) ⊆ 𝑈 → (∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴 → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
2821, 26, 27syl2im 40 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
2928ad2ant2r 782 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
3014, 29sylbid 230 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝐴 ∈ (rank‘𝑥) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
31 simprr 795 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ¬ 𝑥 ∈ (𝑅1𝐴))
32 ne0i 3902 . . . . . . . . . . . . . . 15 (𝑥𝑈𝑈 ≠ ∅)
33 gruina.1 . . . . . . . . . . . . . . . 16 𝐴 = (𝑈 ∩ On)
3433gruina 9591 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
3532, 34sylan2 491 . . . . . . . . . . . . . 14 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ Inacc)
36 inawina 9463 . . . . . . . . . . . . . 14 (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
37 winaon 9461 . . . . . . . . . . . . . 14 (𝐴 ∈ Inaccw𝐴 ∈ On)
3835, 36, 373syl 18 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ On)
39 r1fnon 8581 . . . . . . . . . . . . . 14 𝑅1 Fn On
40 fndm 5953 . . . . . . . . . . . . . 14 (𝑅1 Fn On → dom 𝑅1 = On)
4139, 40ax-mp 5 . . . . . . . . . . . . 13 dom 𝑅1 = On
4238, 41syl6eleqr 2709 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ dom 𝑅1)
4342ad2ant2r 782 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝐴 ∈ dom 𝑅1)
44 rankr1ag 8616 . . . . . . . . . . 11 ((𝑥 (𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) → (𝑥 ∈ (𝑅1𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
4511, 43, 44syl2anc 692 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝑥 ∈ (𝑅1𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
4631, 45mtbid 314 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ¬ (rank‘𝑥) ∈ 𝐴)
47 rankon 8609 . . . . . . . . . . . . 13 (rank‘𝑥) ∈ On
48 eloni 5697 . . . . . . . . . . . . . 14 ((rank‘𝑥) ∈ On → Ord (rank‘𝑥))
49 eloni 5697 . . . . . . . . . . . . . 14 (𝐴 ∈ On → Ord 𝐴)
50 ordtri3or 5719 . . . . . . . . . . . . . 14 ((Ord (rank‘𝑥) ∧ Ord 𝐴) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
5148, 49, 50syl2an 494 . . . . . . . . . . . . 13 (((rank‘𝑥) ∈ On ∧ 𝐴 ∈ On) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
5247, 38, 51sylancr 694 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
53 3orass 1039 . . . . . . . . . . . 12 (((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)) ↔ ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5452, 53sylib 208 . . . . . . . . . . 11 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5554ord 392 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5655ad2ant2r 782 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5746, 56mpd 15 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
586, 30, 57mpjaod 396 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴)
5958ex 450 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → ((𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
6059exlimdv 1858 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (∃𝑥(𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
611, 60syl5bi 232 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (¬ 𝑈 ⊆ (𝑅1𝐴) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
62 simpll 789 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ∈ Univ)
63 ne0i 3902 . . . . . . . . . 10 (𝑦𝑈𝑈 ≠ ∅)
6463, 34sylan2 491 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑦𝑈) → 𝐴 ∈ Inacc)
6564ad2ant2r 782 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ Inacc)
6665, 36, 373syl 18 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ On)
67 simprl 793 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑦𝑈)
68 fveq2 6153 . . . . . . . . . 10 ((rank‘𝑦) = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘𝐴))
6968ad2antll 764 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = (cf‘𝐴))
70 elina 9460 . . . . . . . . . . 11 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴 𝒫 𝑥𝐴))
7170simp2bi 1075 . . . . . . . . . 10 (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
7265, 71syl 17 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘𝐴) = 𝐴)
7369, 72eqtrd 2655 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = 𝐴)
74 rankcf 9550 . . . . . . . . 9 ¬ 𝑦 ≺ (cf‘(rank‘𝑦))
75 fvex 6163 . . . . . . . . . 10 (cf‘(rank‘𝑦)) ∈ V
76 vex 3192 . . . . . . . . . 10 𝑦 ∈ V
77 domtri 9329 . . . . . . . . . 10 (((cf‘(rank‘𝑦)) ∈ V ∧ 𝑦 ∈ V) → ((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦))))
7875, 76, 77mp2an 707 . . . . . . . . 9 ((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦)))
7974, 78mpbir 221 . . . . . . . 8 (cf‘(rank‘𝑦)) ≼ 𝑦
8073, 79syl6eqbrr 4658 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴𝑦)
81 grudomon 9590 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝑦𝑈𝐴𝑦)) → 𝐴𝑈)
8262, 66, 67, 80, 81syl112anc 1327 . . . . . 6 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴𝑈)
83 elin 3779 . . . . . . . . 9 (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴𝑈𝐴 ∈ On))
8483biimpri 218 . . . . . . . 8 ((𝐴𝑈𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On))
8584, 33syl6eleqr 2709 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → 𝐴𝐴)
86 ordirr 5705 . . . . . . . . 9 (Ord 𝐴 → ¬ 𝐴𝐴)
8749, 86syl 17 . . . . . . . 8 (𝐴 ∈ On → ¬ 𝐴𝐴)
8887adantl 482 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → ¬ 𝐴𝐴)
8985, 88pm2.21dd 186 . . . . . 6 ((𝐴𝑈𝐴 ∈ On) → 𝑈 ⊆ (𝑅1𝐴))
9082, 66, 89syl2anc 692 . . . . 5 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ⊆ (𝑅1𝐴))
9190rexlimdvaa 3026 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (∃𝑦𝑈 (rank‘𝑦) = 𝐴𝑈 ⊆ (𝑅1𝐴)))
9261, 91syld 47 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (¬ 𝑈 ⊆ (𝑅1𝐴) → 𝑈 ⊆ (𝑅1𝐴)))
9392pm2.18d 124 . 2 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → 𝑈 ⊆ (𝑅1𝐴))
9433grur1a 9592 . . 3 (𝑈 ∈ Univ → (𝑅1𝐴) ⊆ 𝑈)
9594adantr 481 . 2 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (𝑅1𝐴) ⊆ 𝑈)
9693, 95eqssd 3604 1 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → 𝑈 = (𝑅1𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135   cuni 4407   class class class wbr 4618  Tr wtr 4717  dom cdm 5079  cima 5082  Ord word 5686  Oncon0 5687  Fun wfun 5846   Fn wfn 5847  wf 5848  cfv 5852  cdom 7904  csdm 7905  TCctc 8563  𝑅1cr1 8576  rankcrnk 8577  cfccf 8714  Inaccwcwina 9455  Inacccina 9456  Univcgru 9563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-ac2 9236
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-tc 8564  df-r1 8578  df-rank 8579  df-card 8716  df-cf 8718  df-acn 8719  df-ac 8890  df-wina 9457  df-ina 9458  df-gru 9564
This theorem is referenced by:  grutsk  9595  bj-grur1  32697
  Copyright terms: Public domain W3C validator