Step | Hyp | Ref
| Expression |
1 | | nss 3626 |
. . . . 5
⊢ (¬
𝑈 ⊆
(𝑅1‘𝐴) ↔ ∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) |
2 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (rank‘𝑦) = (rank‘𝑥)) |
3 | 2 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((rank‘𝑦) = 𝐴 ↔ (rank‘𝑥) = 𝐴)) |
4 | 3 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑈 ∧ (rank‘𝑥) = 𝐴) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴) |
5 | 4 | ex 449 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑈 → ((rank‘𝑥) = 𝐴 → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
6 | 5 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ((rank‘𝑥) = 𝐴 → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
7 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑈 ∈ ∪
(𝑅1 “ On)) |
8 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑥 ∈ 𝑈) |
9 | | r1elssi 8551 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ ∪ (𝑅1 “ On) → 𝑈 ⊆ ∪ (𝑅1 “ On)) |
10 | 9 | sseld 3567 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝑈 → 𝑥 ∈ ∪
(𝑅1 “ On))) |
11 | 7, 8, 10 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
12 | | tcrank 8630 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑥) = (rank
“ (TC‘𝑥))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (rank‘𝑥) = (rank “
(TC‘𝑥))) |
14 | 13 | eleq2d 2673 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank‘𝑥) ↔ 𝐴 ∈ (rank “ (TC‘𝑥)))) |
15 | | gruelss 9495 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝑥 ⊆ 𝑈) |
16 | | grutr 9494 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ Univ → Tr 𝑈) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → Tr 𝑈) |
18 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
19 | | tcmin 8500 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V → ((𝑥 ⊆ 𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈) |
21 | 15, 17, 20 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (TC‘𝑥) ⊆ 𝑈) |
22 | | rankf 8540 |
. . . . . . . . . . . . 13
⊢
rank:∪ (𝑅1 “
On)⟶On |
23 | | ffun 5961 |
. . . . . . . . . . . . 13
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
rank |
25 | | fvelima 6158 |
. . . . . . . . . . . 12
⊢ ((Fun
rank ∧ 𝐴 ∈ (rank
“ (TC‘𝑥)))
→ ∃𝑦 ∈
(TC‘𝑥)(rank‘𝑦) = 𝐴) |
26 | 24, 25 | mpan 702 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (rank “
(TC‘𝑥)) →
∃𝑦 ∈
(TC‘𝑥)(rank‘𝑦) = 𝐴) |
27 | | ssrexv 3630 |
. . . . . . . . . . 11
⊢
((TC‘𝑥)
⊆ 𝑈 →
(∃𝑦 ∈
(TC‘𝑥)(rank‘𝑦) = 𝐴 → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
28 | 21, 26, 27 | syl2im 39 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
29 | 28 | ad2ant2r 779 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
30 | 14, 29 | sylbid 229 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝐴 ∈ (rank‘𝑥) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
31 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ¬ 𝑥 ∈
(𝑅1‘𝐴)) |
32 | | ne0i 3880 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑈 → 𝑈 ≠ ∅) |
33 | | gruina.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 = (𝑈 ∩ On) |
34 | 33 | gruina 9519 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) |
35 | 32, 34 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ Inacc) |
36 | | inawina 9391 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Inacc → 𝐴 ∈
Inaccw) |
37 | | winaon 9389 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Inaccw →
𝐴 ∈
On) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ On) |
39 | | r1fnon 8513 |
. . . . . . . . . . . . . 14
⊢
𝑅1 Fn On |
40 | | fndm 5904 |
. . . . . . . . . . . . . 14
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom
𝑅1 = On |
42 | 38, 41 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → 𝐴 ∈ dom
𝑅1) |
43 | 42 | ad2ant2r 779 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → 𝐴 ∈ dom
𝑅1) |
44 | | rankr1ag 8548 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝐴 ∈ dom
𝑅1) → (𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘𝑥) ∈ 𝐴)) |
45 | 11, 43, 44 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘𝑥) ∈ 𝐴)) |
46 | 31, 45 | mtbid 313 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ¬
(rank‘𝑥) ∈ 𝐴) |
47 | | rankon 8541 |
. . . . . . . . . . . . 13
⊢
(rank‘𝑥)
∈ On |
48 | | eloni 5650 |
. . . . . . . . . . . . . 14
⊢
((rank‘𝑥)
∈ On → Ord (rank‘𝑥)) |
49 | | eloni 5650 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → Ord 𝐴) |
50 | | ordtri3or 5672 |
. . . . . . . . . . . . . 14
⊢ ((Ord
(rank‘𝑥) ∧ Ord
𝐴) →
((rank‘𝑥) ∈
𝐴 ∨ (rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))) |
51 | 48, 49, 50 | syl2an 493 |
. . . . . . . . . . . . 13
⊢
(((rank‘𝑥)
∈ On ∧ 𝐴 ∈
On) → ((rank‘𝑥)
∈ 𝐴 ∨
(rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))) |
52 | 47, 38, 51 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))) |
53 | | 3orass 1034 |
. . . . . . . . . . . 12
⊢
(((rank‘𝑥)
∈ 𝐴 ∨
(rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)) ↔ ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))) |
54 | 52, 53 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))) |
55 | 54 | ord 391 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))) |
56 | 55 | ad2ant2r 779 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → (¬
(rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥)))) |
57 | 46, 56 | mpd 15 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ((rank‘𝑥) = 𝐴 ∨ 𝐴 ∈ (rank‘𝑥))) |
58 | 6, 30, 57 | mpjaod 395 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴))) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴) |
59 | 58 | ex 449 |
. . . . . 6
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → ((𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
60 | 59 | exlimdv 1848 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ (𝑅1‘𝐴)) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
61 | 1, 60 | syl5bi 231 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (¬ 𝑈 ⊆
(𝑅1‘𝐴) → ∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴)) |
62 | | simpll 786 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ∈ Univ) |
63 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑈 → 𝑈 ≠ ∅) |
64 | 63, 34 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝑦 ∈ 𝑈) → 𝐴 ∈ Inacc) |
65 | 64 | ad2ant2r 779 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ Inacc) |
66 | 65, 36, 37 | 3syl 18 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ On) |
67 | | simprl 790 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑦 ∈ 𝑈) |
68 | | fveq2 6103 |
. . . . . . . . . 10
⊢
((rank‘𝑦) =
𝐴 →
(cf‘(rank‘𝑦)) =
(cf‘𝐴)) |
69 | 68 | ad2antll 761 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = (cf‘𝐴)) |
70 | | elina 9388 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) |
71 | 70 | simp2bi 1070 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Inacc →
(cf‘𝐴) = 𝐴) |
72 | 65, 71 | syl 17 |
. . . . . . . . 9
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘𝐴) = 𝐴) |
73 | 69, 72 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = 𝐴) |
74 | | rankcf 9478 |
. . . . . . . . 9
⊢ ¬
𝑦 ≺
(cf‘(rank‘𝑦)) |
75 | | fvex 6113 |
. . . . . . . . . 10
⊢
(cf‘(rank‘𝑦)) ∈ V |
76 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
77 | | domtri 9257 |
. . . . . . . . . 10
⊢
(((cf‘(rank‘𝑦)) ∈ V ∧ 𝑦 ∈ V) →
((cf‘(rank‘𝑦))
≼ 𝑦 ↔ ¬
𝑦 ≺
(cf‘(rank‘𝑦)))) |
78 | 75, 76, 77 | mp2an 704 |
. . . . . . . . 9
⊢
((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦))) |
79 | 74, 78 | mpbir 220 |
. . . . . . . 8
⊢
(cf‘(rank‘𝑦)) ≼ 𝑦 |
80 | 73, 79 | syl6eqbrr 4623 |
. . . . . . 7
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ≼ 𝑦) |
81 | | grudomon 9518 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝑦 ∈ 𝑈 ∧ 𝐴 ≼ 𝑦)) → 𝐴 ∈ 𝑈) |
82 | 62, 66, 67, 80, 81 | syl112anc 1322 |
. . . . . 6
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ 𝑈) |
83 | | elin 3758 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On)) |
84 | 83 | biimpri 217 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On)) |
85 | 84, 33 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝐴 ∈ 𝐴) |
86 | | ordirr 5658 |
. . . . . . . . 9
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
87 | 49, 86 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴) |
88 | 87 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → ¬ 𝐴 ∈ 𝐴) |
89 | 85, 88 | pm2.21dd 185 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On) → 𝑈 ⊆ (𝑅1‘𝐴)) |
90 | 82, 66, 89 | syl2anc 691 |
. . . . 5
⊢ (((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) ∧ (𝑦 ∈ 𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ⊆ (𝑅1‘𝐴)) |
91 | 90 | rexlimdvaa 3014 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (∃𝑦 ∈ 𝑈 (rank‘𝑦) = 𝐴 → 𝑈 ⊆ (𝑅1‘𝐴))) |
92 | 61, 91 | syld 46 |
. . 3
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → (¬ 𝑈 ⊆
(𝑅1‘𝐴) → 𝑈 ⊆ (𝑅1‘𝐴))) |
93 | 92 | pm2.18d 123 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 ⊆
(𝑅1‘𝐴)) |
94 | 33 | grur1a 9520 |
. . 3
⊢ (𝑈 ∈ Univ →
(𝑅1‘𝐴) ⊆ 𝑈) |
95 | 94 | adantr 480 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) →
(𝑅1‘𝐴) ⊆ 𝑈) |
96 | 93, 95 | eqssd 3585 |
1
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 =
(𝑅1‘𝐴)) |