Step | Hyp | Ref
| Expression |
1 | | grur1cld.2 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐺) |
2 | 1 | adantr 483 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ On) → 𝐴 ∈ 𝐺) |
3 | | eleq1 2900 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐺 ↔ ∅ ∈ 𝐺)) |
4 | | fveq2 6670 |
. . . . . 6
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) |
5 | 4 | eleq1d 2897 |
. . . . 5
⊢ (𝑥 = ∅ →
((𝑅1‘𝑥) ∈ 𝐺 ↔
(𝑅1‘∅) ∈ 𝐺)) |
6 | 3, 5 | imbi12d 347 |
. . . 4
⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝐺 → (𝑅1‘𝑥) ∈ 𝐺) ↔ (∅ ∈ 𝐺 →
(𝑅1‘∅) ∈ 𝐺))) |
7 | | eleq1 2900 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐺 ↔ 𝑦 ∈ 𝐺)) |
8 | | fveq2 6670 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
9 | 8 | eleq1d 2897 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) ∈ 𝐺 ↔ (𝑅1‘𝑦) ∈ 𝐺)) |
10 | 7, 9 | imbi12d 347 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐺 → (𝑅1‘𝑥) ∈ 𝐺) ↔ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺))) |
11 | | eleq1 2900 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝐺 ↔ suc 𝑦 ∈ 𝐺)) |
12 | | fveq2 6670 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
13 | 12 | eleq1d 2897 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝑥) ∈ 𝐺 ↔ (𝑅1‘suc
𝑦) ∈ 𝐺)) |
14 | 11, 13 | imbi12d 347 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ 𝐺 → (𝑅1‘𝑥) ∈ 𝐺) ↔ (suc 𝑦 ∈ 𝐺 → (𝑅1‘suc
𝑦) ∈ 𝐺))) |
15 | | eleq1 2900 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐺 ↔ 𝐴 ∈ 𝐺)) |
16 | | fveq2 6670 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑅1‘𝑥) =
(𝑅1‘𝐴)) |
17 | 16 | eleq1d 2897 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑅1‘𝑥) ∈ 𝐺 ↔ (𝑅1‘𝐴) ∈ 𝐺)) |
18 | 15, 17 | imbi12d 347 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐺 → (𝑅1‘𝑥) ∈ 𝐺) ↔ (𝐴 ∈ 𝐺 → (𝑅1‘𝐴) ∈ 𝐺))) |
19 | | r10 9197 |
. . . . . . 7
⊢
(𝑅1‘∅) = ∅ |
20 | | grur1cld.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Univ) |
21 | 20, 1 | gru0eld 40614 |
. . . . . . 7
⊢ (𝜑 → ∅ ∈ 𝐺) |
22 | 19, 21 | eqeltrid 2917 |
. . . . . 6
⊢ (𝜑 →
(𝑅1‘∅) ∈ 𝐺) |
23 | 22 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ On) →
(𝑅1‘∅) ∈ 𝐺) |
24 | 23 | a1d 25 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ On) → (∅ ∈ 𝐺 →
(𝑅1‘∅) ∈ 𝐺)) |
25 | | simpl1 1187 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → (𝜑 ∧ 𝐴 ∈ On)) |
26 | | simpl2 1188 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → 𝑦 ∈ On) |
27 | 20 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ On) → 𝐺 ∈ Univ) |
28 | 25, 27 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → 𝐺 ∈ Univ) |
29 | | simpr 487 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → suc 𝑦 ∈ 𝐺) |
30 | | sssucid 6268 |
. . . . . . . . 9
⊢ 𝑦 ⊆ suc 𝑦 |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → 𝑦 ⊆ suc 𝑦) |
32 | | gruss 10218 |
. . . . . . . 8
⊢ ((𝐺 ∈ Univ ∧ suc 𝑦 ∈ 𝐺 ∧ 𝑦 ⊆ suc 𝑦) → 𝑦 ∈ 𝐺) |
33 | 28, 29, 31, 32 | syl3anc 1367 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → 𝑦 ∈ 𝐺) |
34 | | simpl3 1189 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) |
35 | 33, 34 | mpd 15 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → (𝑅1‘𝑦) ∈ 𝐺) |
36 | | r1suc 9199 |
. . . . . . . 8
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) |
37 | 36 | 3ad2ant2 1130 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧
(𝑅1‘𝑦) ∈ 𝐺) → (𝑅1‘suc
𝑦) = 𝒫
(𝑅1‘𝑦)) |
38 | 27 | 3ad2ant1 1129 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧
(𝑅1‘𝑦) ∈ 𝐺) → 𝐺 ∈ Univ) |
39 | | simp3 1134 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧
(𝑅1‘𝑦) ∈ 𝐺) → (𝑅1‘𝑦) ∈ 𝐺) |
40 | | grupw 10217 |
. . . . . . . 8
⊢ ((𝐺 ∈ Univ ∧
(𝑅1‘𝑦) ∈ 𝐺) → 𝒫
(𝑅1‘𝑦) ∈ 𝐺) |
41 | 38, 39, 40 | syl2anc 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧
(𝑅1‘𝑦) ∈ 𝐺) → 𝒫
(𝑅1‘𝑦) ∈ 𝐺) |
42 | 37, 41 | eqeltrd 2913 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧
(𝑅1‘𝑦) ∈ 𝐺) → (𝑅1‘suc
𝑦) ∈ 𝐺) |
43 | 25, 26, 35, 42 | syl3anc 1367 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ suc 𝑦 ∈ 𝐺) → (𝑅1‘suc
𝑦) ∈ 𝐺) |
44 | 43 | ex 415 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ 𝑦 ∈ On ∧ (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) → (suc 𝑦 ∈ 𝐺 → (𝑅1‘suc
𝑦) ∈ 𝐺)) |
45 | | simpr 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺) |
46 | | simpl2 1188 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → Lim 𝑥) |
47 | | r1lim 9201 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐺 ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
48 | 45, 46, 47 | syl2anc 586 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → (𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
49 | | simpl1 1187 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → (𝜑 ∧ 𝐴 ∈ On)) |
50 | 49, 27 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → 𝐺 ∈ Univ) |
51 | | simpl3 1189 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) |
52 | | simpl1l 1220 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → 𝜑) |
53 | | simpl1 1187 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → 𝜑) |
54 | 53, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → 𝐺 ∈ Univ) |
55 | | simpl3 1189 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝐺) |
56 | | simpl2 1188 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → Lim 𝑥) |
57 | | limord 6250 |
. . . . . . . . . . . . 13
⊢ (Lim
𝑥 → Ord 𝑥) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → Ord 𝑥) |
59 | | simpr 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
60 | | ordelss 6207 |
. . . . . . . . . . . 12
⊢ ((Ord
𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥) |
61 | 58, 59, 60 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥) |
62 | | gruss 10218 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Univ ∧ 𝑥 ∈ 𝐺 ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ 𝐺) |
63 | 54, 55, 61, 62 | syl3anc 1367 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐺) |
64 | 63 | ralrimiva 3182 |
. . . . . . . . 9
⊢ ((𝜑 ∧ Lim 𝑥 ∧ 𝑥 ∈ 𝐺) → ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐺) |
65 | 52, 46, 45, 64 | syl3anc 1367 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐺) |
66 | | ralim 3162 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺) → (∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐺 → ∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝐺)) |
67 | 51, 65, 66 | sylc 65 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → ∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝐺) |
68 | | gruiun 10221 |
. . . . . . 7
⊢ ((𝐺 ∈ Univ ∧ 𝑥 ∈ 𝐺 ∧ ∀𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝐺) → ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝐺) |
69 | 50, 45, 67, 68 | syl3anc 1367 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦) ∈ 𝐺) |
70 | 48, 69 | eqeltrd 2913 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) ∧ 𝑥 ∈ 𝐺) → (𝑅1‘𝑥) ∈ 𝐺) |
71 | 70 | ex 415 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ On) ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐺 → (𝑅1‘𝑦) ∈ 𝐺)) → (𝑥 ∈ 𝐺 → (𝑅1‘𝑥) ∈ 𝐺)) |
72 | | simpr 487 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ On) → 𝐴 ∈ On) |
73 | 6, 10, 14, 18, 24, 44, 71, 72 | tfindsd 40613 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ On) → (𝐴 ∈ 𝐺 → (𝑅1‘𝐴) ∈ 𝐺)) |
74 | 2, 73 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ On) →
(𝑅1‘𝐴) ∈ 𝐺) |
75 | | r1fnon 9196 |
. . . . . . 7
⊢
𝑅1 Fn On |
76 | | fndm 6455 |
. . . . . . 7
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
77 | 75, 76 | ax-mp 5 |
. . . . . 6
⊢ dom
𝑅1 = On |
78 | 77 | eleq2i 2904 |
. . . . 5
⊢ (𝐴 ∈ dom
𝑅1 ↔ 𝐴 ∈ On) |
79 | | ndmfv 6700 |
. . . . 5
⊢ (¬
𝐴 ∈ dom
𝑅1 → (𝑅1‘𝐴) = ∅) |
80 | 78, 79 | sylnbir 333 |
. . . 4
⊢ (¬
𝐴 ∈ On →
(𝑅1‘𝐴) = ∅) |
81 | 80 | adantl 484 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ On) →
(𝑅1‘𝐴) = ∅) |
82 | 21 | adantr 483 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ On) → ∅ ∈ 𝐺) |
83 | 81, 82 | eqeltrd 2913 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ On) →
(𝑅1‘𝐴) ∈ 𝐺) |
84 | 74, 83 | pm2.61dan 811 |
1
⊢ (𝜑 →
(𝑅1‘𝐴) ∈ 𝐺) |