Metamath Proof Explorer

Theorem grur1

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

Ref Expression
Hypothesis gruina.1 ⊢ 𝐴 = ( 𝑈 ∩ On )
Assertion grur1 ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → 𝑈 = ( 𝑅1 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 gruina.1 ⊢ 𝐴 = ( 𝑈 ∩ On )
2 nss ⊢ ( ¬ 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
3 fveqeq2 ⊢ ( 𝑦 = 𝑥 → ( ( rank ‘ 𝑦 ) = 𝐴 ↔ ( rank ‘ 𝑥 ) = 𝐴 ) )
4 3 rspcev ⊢ ( ( 𝑥 ∈ 𝑈 ∧ ( rank ‘ 𝑥 ) = 𝐴 ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 )
5 4 ex ⊢ ( 𝑥 ∈ 𝑈 → ( ( rank ‘ 𝑥 ) = 𝐴 → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
6 5 ad2antrl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( ( rank ‘ 𝑥 ) = 𝐴 → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
7 simplr ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → 𝑈 ∈ ∪ ( 𝑅1 “ On ) )
8 simprl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → 𝑥 ∈ 𝑈 )
9 r1elssi ⊢ ( 𝑈 ∈ ∪ ( 𝑅1 “ On ) → 𝑈 ⊆ ∪ ( 𝑅1 “ On ) )
10 9 sseld ⊢ ( 𝑈 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
11 7 8 10 sylc ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
12 tcrank ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝑥 ) = ( rank “ ( TC ‘ 𝑥 ) ) )
13 11 12 syl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( rank ‘ 𝑥 ) = ( rank “ ( TC ‘ 𝑥 ) ) )
14 13 eleq2d ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( 𝐴 ∈ ( rank ‘ 𝑥 ) ↔ 𝐴 ∈ ( rank “ ( TC ‘ 𝑥 ) ) ) )
15 gruelss ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ⊆ 𝑈 )
16 grutr ⊢ ( 𝑈 ∈ Univ → Tr 𝑈 )
17 16 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → Tr 𝑈 )
18 vex ⊢ 𝑥 ∈ V
19 tcmin ⊢ ( 𝑥 ∈ V → ( ( 𝑥 ⊆ 𝑈 ∧ Tr 𝑈 ) → ( TC ‘ 𝑥 ) ⊆ 𝑈 ) )
20 18 19 ax-mp ⊢ ( ( 𝑥 ⊆ 𝑈 ∧ Tr 𝑈 ) → ( TC ‘ 𝑥 ) ⊆ 𝑈 )
21 15 17 20 syl2anc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( TC ‘ 𝑥 ) ⊆ 𝑈 )
22 rankf ⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On
23 ffun ⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → Fun rank )
24 22 23 ax-mp ⊢ Fun rank
25 fvelima ⊢ ( ( Fun rank ∧ 𝐴 ∈ ( rank “ ( TC ‘ 𝑥 ) ) ) → ∃ 𝑦 ∈ ( TC ‘ 𝑥 ) ( rank ‘ 𝑦 ) = 𝐴 )
26 24 25 mpan ⊢ ( 𝐴 ∈ ( rank “ ( TC ‘ 𝑥 ) ) → ∃ 𝑦 ∈ ( TC ‘ 𝑥 ) ( rank ‘ 𝑦 ) = 𝐴 )
27 ssrexv ⊢ ( ( TC ‘ 𝑥 ) ⊆ 𝑈 → ( ∃ 𝑦 ∈ ( TC ‘ 𝑥 ) ( rank ‘ 𝑦 ) = 𝐴 → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
28 21 26 27 syl2im ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( 𝐴 ∈ ( rank “ ( TC ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
29 28 ad2ant2r ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( 𝐴 ∈ ( rank “ ( TC ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
30 14 29 sylbid ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( 𝐴 ∈ ( rank ‘ 𝑥 ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
31 simprr ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) )
32 ne0i ⊢ ( 𝑥 ∈ 𝑈 → 𝑈 ≠ ∅ )
33 1 gruina ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ∈ Inacc )
34 32 33 sylan2 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ∈ Inacc )
35 inawina ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw )
36 winaon ⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On )
37 34 35 36 3syl ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ∈ On )
38 r1fnon ⊢ 𝑅1 Fn On
39 fndm ⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
40 38 39 ax-mp ⊢ dom 𝑅1 = On
41 37 40 eleqtrrdi ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ∈ dom 𝑅1 )
42 41 ad2ant2r ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → 𝐴 ∈ dom 𝑅1 )
43 rankr1ag ⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
44 11 42 43 syl2anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
45 31 44 mtbid ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ¬ ( rank ‘ 𝑥 ) ∈ 𝐴 )
46 rankon ⊢ ( rank ‘ 𝑥 ) ∈ On
47 eloni ⊢ ( ( rank ‘ 𝑥 ) ∈ On → Ord ( rank ‘ 𝑥 ) )
48 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
49 ordtri3or ⊢ ( ( Ord ( rank ‘ 𝑥 ) ∧ Ord 𝐴 ) → ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) )
50 47 48 49 syl2an ⊢ ( ( ( rank ‘ 𝑥 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) )
51 46 37 50 sylancr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) )
52 3orass ⊢ ( ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) ↔ ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) ) )
53 51 52 sylib ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( ( rank ‘ 𝑥 ) ∈ 𝐴 ∨ ( ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) ) )
54 53 ord ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( ¬ ( rank ‘ 𝑥 ) ∈ 𝐴 → ( ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) ) )
55 54 ad2ant2r ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( ¬ ( rank ‘ 𝑥 ) ∈ 𝐴 → ( ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) ) )
56 45 55 mpd ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ( ( rank ‘ 𝑥 ) = 𝐴 ∨ 𝐴 ∈ ( rank ‘ 𝑥 ) ) )
57 6 30 56 mpjaod ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 )
58 57 ex ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → ( ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
59 58 exlimdv ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
60 2 59 syl5bi ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → ( ¬ 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) → ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 ) )
61 simpll ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝑈 ∈ Univ )
62 ne0i ⊢ ( 𝑦 ∈ 𝑈 → 𝑈 ≠ ∅ )
63 62 33 sylan2 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑦 ∈ 𝑈 ) → 𝐴 ∈ Inacc )
64 63 ad2ant2r ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝐴 ∈ Inacc )
65 64 35 36 3syl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝐴 ∈ On )
66 simprl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝑦 ∈ 𝑈 )
67 fveq2 ⊢ ( ( rank ‘ 𝑦 ) = 𝐴 → ( cf ‘ ( rank ‘ 𝑦 ) ) = ( cf ‘ 𝐴 ) )
68 67 ad2antll ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → ( cf ‘ ( rank ‘ 𝑦 ) ) = ( cf ‘ 𝐴 ) )
69 elina ⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )
70 69 simp2bi ⊢ ( 𝐴 ∈ Inacc → ( cf ‘ 𝐴 ) = 𝐴 )
71 64 70 syl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → ( cf ‘ 𝐴 ) = 𝐴 )
72 68 71 eqtrd ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → ( cf ‘ ( rank ‘ 𝑦 ) ) = 𝐴 )
73 rankcf ⊢ ¬ 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) )
74 fvex ⊢ ( cf ‘ ( rank ‘ 𝑦 ) ) ∈ V
75 vex ⊢ 𝑦 ∈ V
76 domtri ⊢ ( ( ( cf ‘ ( rank ‘ 𝑦 ) ) ∈ V ∧ 𝑦 ∈ V ) → ( ( cf ‘ ( rank ‘ 𝑦 ) ) ≼ 𝑦 ↔ ¬ 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) ) )
77 74 75 76 mp2an ⊢ ( ( cf ‘ ( rank ‘ 𝑦 ) ) ≼ 𝑦 ↔ ¬ 𝑦 ≺ ( cf ‘ ( rank ‘ 𝑦 ) ) )
78 73 77 mpbir ⊢ ( cf ‘ ( rank ‘ 𝑦 ) ) ≼ 𝑦
79 72 78 eqbrtrrdi ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝐴 ≼ 𝑦 )
80 grudomon ⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ ( 𝑦 ∈ 𝑈 ∧ 𝐴 ≼ 𝑦 ) ) → 𝐴 ∈ 𝑈 )
81 61 65 66 79 80 syl112anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝐴 ∈ 𝑈 )
82 elin ⊢ ( 𝐴 ∈ ( 𝑈 ∩ On ) ↔ ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) )
83 82 biimpri ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) → 𝐴 ∈ ( 𝑈 ∩ On ) )
84 83 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) → 𝐴 ∈ 𝐴 )
85 ordirr ⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
86 48 85 syl ⊢ ( 𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴 )
87 86 adantl ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) → ¬ 𝐴 ∈ 𝐴 )
88 84 87 pm2.21dd ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) → 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) )
89 81 65 88 syl2anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑦 ∈ 𝑈 ∧ ( rank ‘ 𝑦 ) = 𝐴 ) ) → 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) )
90 89 rexlimdvaa ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → ( ∃ 𝑦 ∈ 𝑈 ( rank ‘ 𝑦 ) = 𝐴 → 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
91 60 90 syld ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → ( ¬ 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) → 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
92 91 pm2.18d ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → 𝑈 ⊆ ( 𝑅1 ‘ 𝐴 ) )
93 1 grur1a ⊢ ( 𝑈 ∈ Univ → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )
94 93 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝑅1 ‘ 𝐴 ) ⊆ 𝑈 )
95 92 94 eqssd ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ ( 𝑅1 “ On ) ) → 𝑈 = ( 𝑅1 ‘ 𝐴 ) )