Proof of Theorem dfac12lem2
| Step | Hyp | Ref
| Expression |
| 1 | | dfac12.4 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) |
| 2 | 1 | tfr1 8437 |
. . . . . . . . . . . . 13
⊢ 𝐺 Fn On |
| 3 | | fnfun 6668 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn On → Fun 𝐺) |
| 4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun 𝐺 |
| 5 | | dfac12.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ On) |
| 6 | | funimaexg 6653 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V) |
| 7 | 4, 5, 6 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 “ 𝐶) ∈ V) |
| 8 | | uniexg 7760 |
. . . . . . . . . . 11
⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺
“ 𝐶) ∈
V) |
| 9 | | rnexg 7924 |
. . . . . . . . . . 11
⊢ (∪ (𝐺
“ 𝐶) ∈ V →
ran ∪ (𝐺 “ 𝐶) ∈ V) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ∈
V) |
| 11 | | dfac12.8 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
| 12 | | f1f 6804 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧):(𝑅1‘𝑧)⟶On) |
| 13 | | fssxp 6763 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)⟶On → (𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On)) |
| 14 | | ssv 4008 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(𝑅1‘𝑧) ⊆ V |
| 15 | | xpss1 5704 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((𝑅1‘𝑧) ⊆ V →
((𝑅1‘𝑧) × On) ⊆ (V ×
On)) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
((𝑅1‘𝑧) × On) ⊆ (V ×
On) |
| 17 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) ∧
((𝑅1‘𝑧) × On) ⊆ (V × On)) →
(𝐺‘𝑧) ⊆ (V × On)) |
| 18 | 16, 17 | mpan2 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ⊆ (V × On)) |
| 19 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺‘𝑧) ∈ V |
| 20 | 19 | elpw 4604 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑧) ∈ 𝒫 (V × On) ↔
(𝐺‘𝑧) ⊆ (V × On)) |
| 21 | 18, 20 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
| 22 | 12, 13, 21 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
| 23 | 22 | ralimi 3083 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
| 24 | 11, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On)) |
| 25 | | onss 7805 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ On → 𝐶 ⊆ On) |
| 26 | 5, 25 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ⊆ On) |
| 27 | 2 | fndmi 6672 |
. . . . . . . . . . . . . . . 16
⊢ dom 𝐺 = On |
| 28 | 26, 27 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ⊆ dom 𝐺) |
| 29 | | funimass4 6973 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐺 ∧ 𝐶 ⊆ dom 𝐺) → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔
∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On))) |
| 30 | 4, 28, 29 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔
∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V ×
On))) |
| 31 | 24, 30 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 “ 𝐶) ⊆ 𝒫 (V ×
On)) |
| 32 | | sspwuni 5100 |
. . . . . . . . . . . . 13
⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔
∪ (𝐺 “ 𝐶) ⊆ (V × On)) |
| 33 | 31, 32 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (𝐺
“ 𝐶) ⊆ (V
× On)) |
| 34 | | rnss 5950 |
. . . . . . . . . . . 12
⊢ (∪ (𝐺
“ 𝐶) ⊆ (V
× On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V ×
On)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ⊆ ran (V
× On)) |
| 36 | | rnxpss 6192 |
. . . . . . . . . . 11
⊢ ran (V
× On) ⊆ On |
| 37 | 35, 36 | sstrdi 3996 |
. . . . . . . . . 10
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ⊆
On) |
| 38 | | ssonuni 7800 |
. . . . . . . . . 10
⊢ (ran
∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺
“ 𝐶) ⊆ On
→ ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)) |
| 39 | 10, 37, 38 | sylc 65 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
| 40 | | onsuc 7831 |
. . . . . . . . 9
⊢ (∪ ran ∪ (𝐺 “ 𝐶) ∈ On → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
| 41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
| 42 | 41 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
| 43 | | rankon 9835 |
. . . . . . 7
⊢
(rank‘𝑦)
∈ On |
| 44 | | omcl 8574 |
. . . . . . 7
⊢ ((suc
∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On) |
| 45 | 42, 43, 44 | sylancl 586 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On) |
| 46 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑧 = suc (rank‘𝑦) → (𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦))) |
| 47 | | f1eq1 6799 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On)) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On)) |
| 49 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑧 = suc (rank‘𝑦) →
(𝑅1‘𝑧) = (𝑅1‘suc
(rank‘𝑦))) |
| 50 | | f1eq2 6800 |
. . . . . . . . . . 11
⊢
((𝑅1‘𝑧) = (𝑅1‘suc
(rank‘𝑦)) →
((𝐺‘suc
(rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
| 52 | 48, 51 | bitrd 279 |
. . . . . . . . 9
⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On)) |
| 53 | 11 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
| 54 | | rankr1ai 9838 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶) |
| 55 | 54 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶) |
| 56 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶) |
| 57 | 55, 56 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶) |
| 58 | | eloni 6394 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ On → Ord 𝐶) |
| 59 | 5, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Ord 𝐶) |
| 60 | 59 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶) |
| 61 | | ordsucuniel 7844 |
. . . . . . . . . . 11
⊢ (Ord
𝐶 → ((rank‘𝑦) ∈ ∪ 𝐶
↔ suc (rank‘𝑦)
∈ 𝐶)) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((rank‘𝑦) ∈ ∪ 𝐶
↔ suc (rank‘𝑦)
∈ 𝐶)) |
| 63 | 57, 62 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc (rank‘𝑦) ∈ 𝐶) |
| 64 | 52, 53, 63 | rspcdva 3623 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On) |
| 65 | | f1f 6804 |
. . . . . . . 8
⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))⟶On) |
| 66 | 64, 65 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))⟶On) |
| 67 | | r1elwf 9836 |
. . . . . . . . 9
⊢ (𝑦 ∈
(𝑅1‘𝐶) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
| 68 | 67 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
| 69 | | rankidb 9840 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈
(𝑅1‘suc (rank‘𝑦))) |
| 70 | 68, 69 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) |
| 71 | 66, 70 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) |
| 72 | | oacl 8573 |
. . . . . 6
⊢ (((suc
∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On) |
| 73 | 45, 71, 72 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On) |
| 74 | | dfac12.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On) |
| 75 | | f1f 6804 |
. . . . . . . 8
⊢ (𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On → 𝐹:𝒫
(har‘(𝑅1‘𝐴))⟶On) |
| 76 | 74, 75 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝒫
(har‘(𝑅1‘𝐴))⟶On) |
| 77 | 76 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫
(har‘(𝑅1‘𝐴))⟶On) |
| 78 | | imassrn 6089 |
. . . . . . . 8
⊢ (𝐻 “ 𝑦) ⊆ ran 𝐻 |
| 79 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘∪ 𝐶)
∈ V |
| 80 | 79 | rnex 7932 |
. . . . . . . . . . . . . 14
⊢ ran
(𝐺‘∪ 𝐶)
∈ V |
| 81 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ∪
𝐶 → (𝐺‘𝑧) = (𝐺‘∪ 𝐶)) |
| 82 | | f1eq1 6799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺‘𝑧) = (𝐺‘∪ 𝐶) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On)) |
| 83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ∪
𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On)) |
| 84 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ∪
𝐶 →
(𝑅1‘𝑧) = (𝑅1‘∪ 𝐶)) |
| 85 | | f1eq2 6800 |
. . . . . . . . . . . . . . . . . . 19
⊢
((𝑅1‘𝑧) = (𝑅1‘∪ 𝐶)
→ ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ∪
𝐶 → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
| 87 | 83, 86 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ∪
𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)) |
| 88 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) |
| 89 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ∈ On) |
| 90 | | onuni 7808 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ On → ∪ 𝐶
∈ On) |
| 91 | | sucidg 6465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝐶
∈ On → ∪ 𝐶 ∈ suc ∪
𝐶) |
| 92 | 89, 90, 91 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ suc ∪ 𝐶) |
| 93 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶) |
| 94 | | orduniorsuc 7850 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Ord
𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
| 96 | 95 | orcanai 1005 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶) |
| 97 | 92, 96 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐶) |
| 98 | 87, 88, 97 | rspcdva 3623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On) |
| 99 | | f1f 6804 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On) |
| 100 | | frn 6743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On → ran (𝐺‘∪ 𝐶) ⊆ On) |
| 101 | 98, 99, 100 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ⊆ On) |
| 102 | | epweon 7795 |
. . . . . . . . . . . . . . 15
⊢ E We
On |
| 103 | | wess 5671 |
. . . . . . . . . . . . . . 15
⊢ (ran
(𝐺‘∪ 𝐶)
⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶))) |
| 104 | 101, 102,
103 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶)) |
| 105 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ OrdIso( E
, ran (𝐺‘∪ 𝐶))
= OrdIso( E , ran (𝐺‘∪ 𝐶)) |
| 106 | 105 | oiiso 9577 |
. . . . . . . . . . . . . 14
⊢ ((ran
(𝐺‘∪ 𝐶)
∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶))
Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶))) |
| 107 | 80, 104, 106 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → OrdIso( E , ran (𝐺‘∪ 𝐶))
Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶))) |
| 108 | | isof1o 7343 |
. . . . . . . . . . . . 13
⊢ (OrdIso(
E , ran (𝐺‘∪ 𝐶))
Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran
(𝐺‘∪ 𝐶)) |
| 109 | | f1ocnv 6860 |
. . . . . . . . . . . . 13
⊢ (OrdIso(
E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran
(𝐺‘∪ 𝐶)
→ ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom
OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 110 | | f1of1 6847 |
. . . . . . . . . . . . 13
⊢ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom
OrdIso( E , ran (𝐺‘∪ 𝐶)) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 111 | 107, 108,
109, 110 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 112 | | f1f1orn 6859 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran
(𝐺‘∪ 𝐶)) |
| 113 | | f1of1 6847 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran
(𝐺‘∪ 𝐶)
→ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) |
| 114 | 98, 112, 113 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) |
| 115 | | f1co 6815 |
. . . . . . . . . . . 12
⊢ ((◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 116 | 111, 114,
115 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 117 | | dfac12.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) |
| 118 | | f1eq1 6799 |
. . . . . . . . . . . 12
⊢ (𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) → (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))) |
| 119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 120 | 116, 119 | sylibr 234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 121 | | f1f 6804 |
. . . . . . . . . 10
⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → 𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 122 | | frn 6743 |
. . . . . . . . . 10
⊢ (𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶))
→ ran 𝐻 ⊆ dom
OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 123 | 120, 121,
122 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 124 | | harcl 9599 |
. . . . . . . . . . 11
⊢
(har‘(𝑅1‘𝐴)) ∈ On |
| 125 | 124 | onordi 6495 |
. . . . . . . . . 10
⊢ Ord
(har‘(𝑅1‘𝐴)) |
| 126 | 105 | oion 9576 |
. . . . . . . . . . . 12
⊢ (ran
(𝐺‘∪ 𝐶)
∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On) |
| 127 | 80, 126 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
∈ On) |
| 128 | 105 | oien 9578 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝐺‘∪ 𝐶)
∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
≈ ran (𝐺‘∪ 𝐶)) |
| 129 | 80, 104, 128 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
≈ ran (𝐺‘∪ 𝐶)) |
| 130 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1‘∪ 𝐶) ∈ V |
| 131 | 130 | f1oen 9013 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran
(𝐺‘∪ 𝐶)
→ (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶)) |
| 132 | | ensym 9043 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈
(𝑅1‘∪ 𝐶)) |
| 133 | 98, 112, 131, 132 | 4syl 19 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈
(𝑅1‘∪ 𝐶)) |
| 134 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(𝑅1‘𝐴) ∈ V |
| 135 | | dfac12.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ On) |
| 136 | 135 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐴 ∈ On) |
| 137 | | dfac12.6 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
| 138 | 137 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ 𝐴) |
| 139 | 138, 97 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐴) |
| 140 | | r1ord2 9821 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → (∪ 𝐶
∈ 𝐴 →
(𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))) |
| 141 | 136, 139,
140 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)) |
| 142 | | ssdomg 9040 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘𝐴) ∈ V →
((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) →
(𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))) |
| 143 | 134, 141,
142 | mpsyl 68 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) |
| 144 | | endomtr 9052 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝐺‘∪ 𝐶)
≈ (𝑅1‘∪ 𝐶) ∧
(𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼
(𝑅1‘𝐴)) |
| 145 | 133, 143,
144 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼
(𝑅1‘𝐴)) |
| 146 | | endomtr 9052 |
. . . . . . . . . . . 12
⊢ ((dom
OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶)
∧ ran (𝐺‘∪ 𝐶)
≼ (𝑅1‘𝐴)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶))
≼ (𝑅1‘𝐴)) |
| 147 | 129, 145,
146 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
≼ (𝑅1‘𝐴)) |
| 148 | | elharval 9601 |
. . . . . . . . . . 11
⊢ (dom
OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈
(har‘(𝑅1‘𝐴)) ↔ (dom OrdIso( E , ran (𝐺‘∪ 𝐶))
∈ On ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼
(𝑅1‘𝐴))) |
| 149 | 127, 147,
148 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
∈ (har‘(𝑅1‘𝐴))) |
| 150 | | ordelss 6400 |
. . . . . . . . . 10
⊢ ((Ord
(har‘(𝑅1‘𝐴)) ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶))
∈ (har‘(𝑅1‘𝐴))) → dom OrdIso( E , ran (𝐺‘∪ 𝐶))
⊆ (har‘(𝑅1‘𝐴))) |
| 151 | 125, 149,
150 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran
(𝐺‘∪ 𝐶))
⊆ (har‘(𝑅1‘𝐴))) |
| 152 | 123, 151 | sstrd 3994 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆
(har‘(𝑅1‘𝐴))) |
| 153 | 78, 152 | sstrid 3995 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆
(har‘(𝑅1‘𝐴))) |
| 154 | | fvex 6919 |
. . . . . . . 8
⊢
(har‘(𝑅1‘𝐴)) ∈ V |
| 155 | 154 | elpw2 5334 |
. . . . . . 7
⊢ ((𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆
(har‘(𝑅1‘𝐴))) |
| 156 | 153, 155 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
| 157 | 77, 156 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On) |
| 158 | 73, 157 | ifclda 4561 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On) |
| 159 | 158 | ex 412 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On)) |
| 160 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝐶 = ∪
𝐶 → if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦))) |
| 161 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝐶 = ∪
𝐶 → if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧))) |
| 162 | 160, 161 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝐶 = ∪
𝐶 → (if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ ((suc ∪
ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
| 163 | 162 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ ((suc ∪
ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
| 164 | 41 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On) |
| 165 | | nsuceq0 6467 |
. . . . . . . 8
⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅ |
| 166 | 165 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅) |
| 167 | 43 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On) |
| 168 | | onsucuni 7848 |
. . . . . . . . . . 11
⊢ (ran
∪ (𝐺 “ 𝐶) ⊆ On → ran ∪ (𝐺
“ 𝐶) ⊆ suc
∪ ran ∪ (𝐺 “ 𝐶)) |
| 169 | 37, 168 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ran ∪ (𝐺
“ 𝐶) ⊆ suc
∪ ran ∪ (𝐺 “ 𝐶)) |
| 170 | 169 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran ∪ (𝐺
“ 𝐶) ⊆ suc
∪ ran ∪ (𝐺 “ 𝐶)) |
| 171 | 26 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ On) |
| 172 | | fnfvima 7253 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶)) |
| 173 | 2, 171, 63, 172 | mp3an2i 1468 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶)) |
| 174 | | elssuni 4937 |
. . . . . . . . . . 11
⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪
(𝐺 “ 𝐶)) |
| 175 | | rnss 5950 |
. . . . . . . . . . 11
⊢ ((𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺
“ 𝐶) → ran
(𝐺‘suc
(rank‘𝑦)) ⊆ ran
∪ (𝐺 “ 𝐶)) |
| 176 | 173, 174,
175 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪
(𝐺 “ 𝐶)) |
| 177 | | f1fn 6805 |
. . . . . . . . . . . 12
⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc
(rank‘𝑦))) |
| 178 | 64, 177 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc
(rank‘𝑦))) |
| 179 | | fnfvelrn 7100 |
. . . . . . . . . . 11
⊢ (((𝐺‘suc (rank‘𝑦)) Fn
(𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) →
((𝐺‘suc
(rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦))) |
| 180 | 178, 70, 179 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦))) |
| 181 | 176, 180 | sseldd 3984 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪
(𝐺 “ 𝐶)) |
| 182 | 170, 181 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
| 183 | 182 | adantlrr 721 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
| 184 | | rankon 9835 |
. . . . . . . 8
⊢
(rank‘𝑧)
∈ On |
| 185 | 184 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On) |
| 186 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1‘𝐶) ↔ 𝑧 ∈ (𝑅1‘𝐶))) |
| 187 | 186 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ↔ (𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)))) |
| 188 | 187 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶))) |
| 189 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧)) |
| 190 | | suceq 6450 |
. . . . . . . . . . . . . 14
⊢
((rank‘𝑦) =
(rank‘𝑧) → suc
(rank‘𝑦) = suc
(rank‘𝑧)) |
| 191 | 189, 190 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧)) |
| 192 | 191 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧))) |
| 193 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
| 194 | 192, 193 | fveq12d 6913 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) |
| 195 | 194 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶))) |
| 196 | 188, 195 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)))) |
| 197 | 196, 182 | chvarvv 1998 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
| 198 | 197 | adantlrl 720 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) |
| 199 | | omopth2 8622 |
. . . . . . 7
⊢ (((suc
∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅) ∧ ((rank‘𝑦) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶)) ∧ ((rank‘𝑧) ∈ On ∧ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran
∪ (𝐺 “ 𝐶))) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
| 200 | 164, 166,
167, 183, 185, 198, 199 | syl222anc 1388 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))) |
| 201 | 190 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧)) |
| 202 | 201 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧))) |
| 203 | 202 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) |
| 204 | 203 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))) |
| 205 | 64 | adantlrr 721 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On) |
| 206 | 205 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On) |
| 207 | 70 | adantlrr 721 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) |
| 208 | 207 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc
(rank‘𝑦))) |
| 209 | | r1elwf 9836 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈
(𝑅1‘𝐶) → 𝑧 ∈ ∪
(𝑅1 “ On)) |
| 210 | | rankidb 9840 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ∈
(𝑅1‘suc (rank‘𝑧))) |
| 211 | 209, 210 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(𝑅1‘𝐶) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑧))) |
| 212 | 211 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑧))) |
| 213 | 212 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑧))) |
| 214 | 201 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) →
(𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc
(rank‘𝑧))) |
| 215 | 213, 214 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc
(rank‘𝑦))) |
| 216 | | f1fveq 7282 |
. . . . . . . . . . 11
⊢ (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc
(rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc
(rank‘𝑦)) ∧ 𝑧 ∈
(𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧)) |
| 217 | 206, 208,
215, 216 | syl12anc 837 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧)) |
| 218 | 204, 217 | bitr3d 281 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧)) |
| 219 | 218 | biimpd 229 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧)) |
| 220 | 219 | expimpd 453 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧)) |
| 221 | 189, 194 | jca 511 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))) |
| 222 | 220, 221 | impbid1 225 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧)) |
| 223 | 163, 200,
222 | 3bitrd 305 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)) |
| 224 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
𝐶 = ∪ 𝐶
→ if(𝐶 = ∪ 𝐶,
((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦))) |
| 225 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
𝐶 = ∪ 𝐶
→ if(𝐶 = ∪ 𝐶,
((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧))) |
| 226 | 224, 225 | eqeq12d 2753 |
. . . . . . 7
⊢ (¬
𝐶 = ∪ 𝐶
→ (if(𝐶 = ∪ 𝐶,
((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)))) |
| 227 | 226 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)))) |
| 228 | 74 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On) |
| 229 | 156 | adantlrr 721 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
| 230 | 187 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶))) |
| 231 | | imaeq2 6074 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧)) |
| 232 | 231 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴)))) |
| 233 | 230, 232 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴))))) |
| 234 | 233, 156 | chvarvv 1998 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
| 235 | 234 | adantlrl 720 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴))) |
| 236 | | f1fveq 7282 |
. . . . . . 7
⊢ ((𝐹:𝒫
(har‘(𝑅1‘𝐴))–1-1→On ∧ ((𝐻 “ 𝑦) ∈ 𝒫
(har‘(𝑅1‘𝐴)) ∧ (𝐻 “ 𝑧) ∈ 𝒫
(har‘(𝑅1‘𝐴)))) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧))) |
| 237 | 228, 229,
235, 236 | syl12anc 837 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧))) |
| 238 | 120 | adantlrr 721 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))) |
| 239 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑦 ∈
(𝑅1‘𝐶)) |
| 240 | 96 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘𝐶) = (𝑅1‘suc ∪ 𝐶)) |
| 241 | | r1suc 9810 |
. . . . . . . . . . . 12
⊢ (∪ 𝐶
∈ On → (𝑅1‘suc ∪
𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
| 242 | 89, 90, 241 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘suc ∪ 𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
| 243 | 240, 242 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) →
(𝑅1‘𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
| 244 | 243 | adantlrr 721 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) →
(𝑅1‘𝐶) = 𝒫
(𝑅1‘∪ 𝐶)) |
| 245 | 239, 244 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑦 ∈ 𝒫
(𝑅1‘∪ 𝐶)) |
| 246 | 245 | elpwid 4609 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑦 ⊆
(𝑅1‘∪ 𝐶)) |
| 247 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑧 ∈
(𝑅1‘𝐶)) |
| 248 | 247, 244 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑧 ∈ 𝒫
(𝑅1‘∪ 𝐶)) |
| 249 | 248 | elpwid 4609 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → 𝑧 ⊆
(𝑅1‘∪ 𝐶)) |
| 250 | | f1imaeq 7285 |
. . . . . . 7
⊢ ((𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝑦 ⊆ (𝑅1‘∪ 𝐶)
∧ 𝑧 ⊆
(𝑅1‘∪ 𝐶))) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧)) |
| 251 | 238, 246,
249, 250 | syl12anc 837 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧)) |
| 252 | 227, 237,
251 | 3bitrd 305 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪
𝐶) → (if(𝐶 = ∪
𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)) |
| 253 | 223, 252 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)) |
| 254 | 253 | ex 412 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶)) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))) |
| 255 | 159, 254 | dom2lem 9032 |
. 2
⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On) |
| 256 | 135, 74, 1, 5, 117 | dfac12lem1 10184 |
. . 3
⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))))) |
| 257 | | f1eq1 6799 |
. . 3
⊢ ((𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))) → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)) |
| 258 | 256, 257 | syl 17 |
. 2
⊢ (𝜑 → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)) |
| 259 | 255, 258 | mpbird 257 |
1
⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On) |