| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nss 4047 | . . . . 5
⊢ (¬
𝑈 ⊆
(𝑅1‘𝐴) ↔ ∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) | 
| 2 |  | fveqeq2 6914 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((rank‘𝑦) = 𝐴 ↔ (rank‘𝑥) = 𝐴)) | 
| 3 | 2 | rspcev 3621 | . . . . . . . . . 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 9846 | . . . . . . . . . . . . 13
⊢ (𝑈 ∈ ∪ (𝑅1 “ On) → 𝑈 ⊆ ∪ (𝑅1 “ On)) | 
| 9 | 8 | sseld 3981 | . . . . . . . . . . . 12
⊢ (𝑈 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝑈 → 𝑥 ∈ ∪
(𝑅1 “ On))) | 
| 10 | 6, 7, 9 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑥 ∈ ∪
(𝑅1 “ On)) | 
| 11 |  | tcrank 9925 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑥) = (rank
“ (TC‘𝑥))) | 
| 12 | 10, 11 | syl 17 | . . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (rank‘𝑥) = (rank “
(TC‘𝑥))) | 
| 13 | 12 | eleq2d 2826 | . . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank‘𝑥) ↔ 𝐴 ∈ (rank “ (TC‘𝑥)))) | 
| 14 |  | gruelss 10835 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝑥 ⊆ 𝑈) | 
| 15 |  | grutr 10834 | . . . . . . . . . . . . 13
⊢ (𝑈 ∈ Univ → Tr 𝑈) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → Tr 𝑈) | 
| 17 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 18 |  | tcmin 9782 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ V → ((𝑥 ⊆ 𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈)) | 
| 19 | 17, 18 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈) | 
| 20 | 14, 16, 19 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (TC‘𝑥) ⊆ 𝑈) | 
| 21 |  | rankf 9835 | . . . . . . . . . . . . 13
⊢
rank:∪ (𝑅1 “
On)⟶On | 
| 22 |  | ffun 6738 | . . . . . . . . . . . . 13
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) | 
| 23 | 21, 22 | ax-mp 5 | . . . . . . . . . . . 12
⊢ Fun
rank | 
| 24 |  | fvelima 6973 | . . . . . . . . . . . 12
⊢ ((Fun
rank ∧ 𝐴 ∈ (rank
“ (TC‘𝑥)))
→ ∃𝑦 ∈
(TC‘𝑥)(rank‘𝑦) = 𝐴) | 
| 25 | 23, 24 | mpan 690 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (rank “
(TC‘𝑥)) →
∃𝑦 ∈
(TC‘𝑥)(rank‘𝑦) = 𝐴) | 
| 26 |  | ssrexv 4052 | . . . . . . . . . . 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 4340 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑈 → 𝑈 ≠ ∅) | 
| 32 |  | gruina.1 | . . . . . . . . . . . . . . . 16
⊢ 𝐴 = (𝑈 ∩ On) | 
| 33 | 32 | gruina 10859 | . . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) | 
| 34 | 31, 33 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ Inacc) | 
| 35 |  | inawina 10731 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Inacc → 𝐴 ∈
Inaccw) | 
| 36 |  | winaon 10729 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Inaccw →
𝐴 ∈
On) | 
| 37 | 34, 35, 36 | 3syl 18 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ On) | 
| 38 |  | r1fnon 9808 | . . . . . . . . . . . . . 14
⊢
𝑅1 Fn On | 
| 39 |  | fndm 6670 | . . . . . . . . . . . . . 14
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) | 
| 40 | 38, 39 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ dom
𝑅1 = On | 
| 41 | 37, 40 | eleqtrrdi 2851 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ dom
𝑅1) | 
| 42 | 41 | ad2ant2r 747 | . . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝐴 ∈ dom
𝑅1) | 
| 43 |  | rankr1ag 9843 | . . . . . . . . . . 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 9836 | . . . . . . . . . . . . 13
⊢
(rank‘𝑥)
∈ On | 
| 47 |  | eloni 6393 | . . . . . . . . . . . . . 14
⊢
((rank‘𝑥)
∈ On → Ord (rank‘𝑥)) | 
| 48 |  | eloni 6393 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → Ord 𝐴) | 
| 49 |  | ordtri3or 6415 | . . . . . . . . . . . . . 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 1932 | . . . . 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 4340 | . . . . . . . . . 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 6905 | . . . . . . . . . 10
⊢
((rank‘𝑦) =
𝐴 →
(cf‘(rank‘𝑦)) =
(cf‘𝐴)) | 
| 68 | 67 | ad2antll 729 | . . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = (cf‘𝐴)) | 
| 69 |  | elina 10728 | . . . . . . . . . . 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 2776 | . . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = 𝐴) | 
| 73 |  | rankcf 10818 | . . . . . . . . 9
⊢  ¬
𝑦 ≺
(cf‘(rank‘𝑦)) | 
| 74 |  | fvex 6918 | . . . . . . . . . 10
⊢
(cf‘(rank‘𝑦)) ∈ V | 
| 75 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 76 |  | domtri 10597 | . . . . . . . . . 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 5182 | . . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ≼ 𝑦) | 
| 80 |  | grudomon 10858 | . . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝑦 ∈ 𝑈 ∧ 𝐴 ≼ 𝑦)) → 𝐴 ∈ 𝑈) | 
| 81 | 61, 65, 66, 79, 80 | syl112anc 1375 | . . . . . 6
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ 𝑈) | 
| 82 |  | elin 3966 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On)) | 
| 83 | 82 | biimpri 228 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On)) | 
| 84 | 83, 32 | eleqtrrdi 2851 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ 𝐴) | 
| 85 |  | ordirr 6401 | . . . . . . . . 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 3155 | . . . 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 10860 | . . 3
⊢ (𝑈 ∈ Univ →
(𝑅1‘𝐴) ⊆ 𝑈) | 
| 94 | 93 | adantr 480 | . 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) →
(𝑅1‘𝐴) ⊆ 𝑈) | 
| 95 | 92, 94 | eqssd 4000 | 1
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 =
(𝑅1‘𝐴)) |