| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . 4
⊢ (𝐺‘𝐴) ∈ V |
| 2 | 1 | rnex 7932 |
. . 3
⊢ ran
(𝐺‘𝐴) ∈ V |
| 3 | | ssid 4006 |
. . . . 5
⊢ 𝐴 ⊆ 𝐴 |
| 4 | | dfac12.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ On) |
| 5 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝐴 ↔ 𝑛 ⊆ 𝐴)) |
| 6 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝐺‘𝑚) = (𝐺‘𝑛)) |
| 7 | | f1eq1 6799 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑚) = (𝐺‘𝑛) → ((𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝑛):(𝑅1‘𝑚)–1-1→On)) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝑛):(𝑅1‘𝑚)–1-1→On)) |
| 9 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑅1‘𝑚) =
(𝑅1‘𝑛)) |
| 10 | | f1eq2 6800 |
. . . . . . . . . . 11
⊢
((𝑅1‘𝑚) = (𝑅1‘𝑛) → ((𝐺‘𝑛):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝐺‘𝑛):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) |
| 12 | 8, 11 | bitrd 279 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) |
| 13 | 5, 12 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On) ↔ (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On))) |
| 14 | 13 | imbi2d 340 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((𝜑 → (𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)) ↔ (𝜑 → (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)))) |
| 15 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑚 = 𝐴 → (𝑚 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
| 16 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝐴 → (𝐺‘𝑚) = (𝐺‘𝐴)) |
| 17 | | f1eq1 6799 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑚) = (𝐺‘𝐴) → ((𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝐴):(𝑅1‘𝑚)–1-1→On)) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐴 → ((𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝐴):(𝑅1‘𝑚)–1-1→On)) |
| 19 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝐴 → (𝑅1‘𝑚) =
(𝑅1‘𝐴)) |
| 20 | | f1eq2 6800 |
. . . . . . . . . . 11
⊢
((𝑅1‘𝑚) = (𝑅1‘𝐴) → ((𝐺‘𝐴):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On)) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐴 → ((𝐺‘𝐴):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On)) |
| 22 | 18, 21 | bitrd 279 |
. . . . . . . . 9
⊢ (𝑚 = 𝐴 → ((𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On ↔ (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On)) |
| 23 | 15, 22 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑚 = 𝐴 → ((𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On) ↔ (𝐴 ⊆ 𝐴 → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On))) |
| 24 | 23 | imbi2d 340 |
. . . . . . 7
⊢ (𝑚 = 𝐴 → ((𝜑 → (𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On)))) |
| 25 | | r19.21v 3180 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝑚 (𝜑 → (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) ↔ (𝜑 → ∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On))) |
| 26 | | eloni 6394 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ On → Ord 𝑚) |
| 27 | 26 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) → Ord 𝑚) |
| 28 | | ordelss 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝑚 ∧ 𝑛 ∈ 𝑚) → 𝑛 ⊆ 𝑚) |
| 29 | 27, 28 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ 𝑛 ∈ 𝑚) → 𝑛 ⊆ 𝑚) |
| 30 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ 𝑛 ∈ 𝑚) → 𝑚 ⊆ 𝐴) |
| 31 | 29, 30 | sstrd 3994 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ 𝑛 ∈ 𝑚) → 𝑛 ⊆ 𝐴) |
| 32 | | pm5.5 361 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ⊆ 𝐴 → ((𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) ↔ (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ 𝑛 ∈ 𝑚) → ((𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) ↔ (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) |
| 34 | 33 | ralbidva 3176 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) → (∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) ↔ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) |
| 35 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → 𝐴 ∈ On) |
| 36 | | dfac12.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → 𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On) |
| 38 | | dfac12.4 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) |
| 39 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → 𝑚 ∈ On) |
| 40 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (◡OrdIso( E , ran (𝐺‘∪ 𝑚)) ∘ (𝐺‘∪ 𝑚)) = (◡OrdIso( E , ran (𝐺‘∪ 𝑚)) ∘ (𝐺‘∪ 𝑚)) |
| 41 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → 𝑚 ⊆ 𝐴) |
| 42 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑧 → (𝐺‘𝑛) = (𝐺‘𝑧)) |
| 44 | | f1eq1 6799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺‘𝑛) = (𝐺‘𝑧) → ((𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On ↔ (𝐺‘𝑧):(𝑅1‘𝑛)–1-1→On)) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → ((𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On ↔ (𝐺‘𝑧):(𝑅1‘𝑛)–1-1→On)) |
| 46 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑧 → (𝑅1‘𝑛) =
(𝑅1‘𝑧)) |
| 47 | | f1eq2 6800 |
. . . . . . . . . . . . . . . . . . 19
⊢
((𝑅1‘𝑛) = (𝑅1‘𝑧) → ((𝐺‘𝑧):(𝑅1‘𝑛)–1-1→On ↔ (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → ((𝐺‘𝑧):(𝑅1‘𝑛)–1-1→On ↔ (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)) |
| 49 | 45, 48 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑧 → ((𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On ↔ (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)) |
| 50 | 49 | cbvralvw 3237 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On ↔ ∀𝑧 ∈ 𝑚 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
| 51 | 42, 50 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → ∀𝑧 ∈ 𝑚 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
| 52 | 35, 37, 38, 39, 40, 41, 51 | dfac12lem2 10185 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) ∧ ∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On) |
| 53 | 52 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) → (∀𝑛 ∈ 𝑚 (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)) |
| 54 | 34, 53 | sylbid 240 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴)) → (∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)) |
| 55 | 54 | expr 456 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ On) → (𝑚 ⊆ 𝐴 → (∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On))) |
| 56 | 55 | com23 86 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ On) → (∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → (𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On))) |
| 57 | 56 | expcom 413 |
. . . . . . . . 9
⊢ (𝑚 ∈ On → (𝜑 → (∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On) → (𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)))) |
| 58 | 57 | a2d 29 |
. . . . . . . 8
⊢ (𝑚 ∈ On → ((𝜑 → ∀𝑛 ∈ 𝑚 (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) → (𝜑 → (𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)))) |
| 59 | 25, 58 | biimtrid 242 |
. . . . . . 7
⊢ (𝑚 ∈ On → (∀𝑛 ∈ 𝑚 (𝜑 → (𝑛 ⊆ 𝐴 → (𝐺‘𝑛):(𝑅1‘𝑛)–1-1→On)) → (𝜑 → (𝑚 ⊆ 𝐴 → (𝐺‘𝑚):(𝑅1‘𝑚)–1-1→On)))) |
| 60 | 14, 24, 59 | tfis3 7879 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝜑 → (𝐴 ⊆ 𝐴 → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On))) |
| 61 | 4, 60 | mpcom 38 |
. . . . 5
⊢ (𝜑 → (𝐴 ⊆ 𝐴 → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On)) |
| 62 | 3, 61 | mpi 20 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On) |
| 63 | | f1f 6804 |
. . . 4
⊢ ((𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On → (𝐺‘𝐴):(𝑅1‘𝐴)⟶On) |
| 64 | | frn 6743 |
. . . 4
⊢ ((𝐺‘𝐴):(𝑅1‘𝐴)⟶On → ran (𝐺‘𝐴) ⊆ On) |
| 65 | 62, 63, 64 | 3syl 18 |
. . 3
⊢ (𝜑 → ran (𝐺‘𝐴) ⊆ On) |
| 66 | | onssnum 10080 |
. . 3
⊢ ((ran
(𝐺‘𝐴) ∈ V ∧ ran (𝐺‘𝐴) ⊆ On) → ran (𝐺‘𝐴) ∈ dom card) |
| 67 | 2, 65, 66 | sylancr 587 |
. 2
⊢ (𝜑 → ran (𝐺‘𝐴) ∈ dom card) |
| 68 | | f1f1orn 6859 |
. . . 4
⊢ ((𝐺‘𝐴):(𝑅1‘𝐴)–1-1→On → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1-onto→ran
(𝐺‘𝐴)) |
| 69 | 62, 68 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺‘𝐴):(𝑅1‘𝐴)–1-1-onto→ran
(𝐺‘𝐴)) |
| 70 | | fvex 6919 |
. . . 4
⊢
(𝑅1‘𝐴) ∈ V |
| 71 | 70 | f1oen 9013 |
. . 3
⊢ ((𝐺‘𝐴):(𝑅1‘𝐴)–1-1-onto→ran
(𝐺‘𝐴) → (𝑅1‘𝐴) ≈ ran (𝐺‘𝐴)) |
| 72 | | ennum 9987 |
. . 3
⊢
((𝑅1‘𝐴) ≈ ran (𝐺‘𝐴) → ((𝑅1‘𝐴) ∈ dom card ↔ ran
(𝐺‘𝐴) ∈ dom card)) |
| 73 | 69, 71, 72 | 3syl 18 |
. 2
⊢ (𝜑 →
((𝑅1‘𝐴) ∈ dom card ↔ ran (𝐺‘𝐴) ∈ dom card)) |
| 74 | 67, 73 | mpbird 257 |
1
⊢ (𝜑 →
(𝑅1‘𝐴) ∈ dom card) |