| Step | Hyp | Ref
| Expression |
| 1 | | pwfseqlem5.g |
. 2
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 2 | | pwfseqlem5.x |
. 2
⊢ (𝜑 → 𝑋 ⊆ 𝐴) |
| 3 | | pwfseqlem5.h |
. 2
⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) |
| 4 | | pwfseqlem5.ps |
. 2
⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) |
| 5 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
| 6 | | simprl3 1221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡) |
| 7 | 4, 6 | sylan2b 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡) |
| 8 | | pwfseqlem5.o |
. . . . . . . . . . . 12
⊢ 𝑂 = OrdIso(𝑟, 𝑡) |
| 9 | 8 | oiiso 9577 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡)) |
| 10 | 5, 7, 9 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡)) |
| 11 | | isof1o 7343 |
. . . . . . . . . 10
⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡) |
| 13 | | cardom 10026 |
. . . . . . . . . . . 12
⊢
(card‘ω) = ω |
| 14 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡) |
| 15 | 4, 14 | sylan2b 594 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡) |
| 16 | 8 | oien 9578 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡) |
| 17 | 5, 7, 16 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡) |
| 18 | 17 | ensymd 9045 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂) |
| 19 | | domentr 9053 |
. . . . . . . . . . . . . 14
⊢ ((ω
≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂) |
| 20 | 15, 18, 19 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂) |
| 21 | | omelon 9686 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
| 22 | | onenon 9989 |
. . . . . . . . . . . . . . 15
⊢ (ω
∈ On → ω ∈ dom card) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ω
∈ dom card |
| 24 | 8 | oion 9576 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ V → dom 𝑂 ∈ On) |
| 25 | 24 | elv 3485 |
. . . . . . . . . . . . . . 15
⊢ dom 𝑂 ∈ On |
| 26 | | onenon 9989 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑂 ∈ On → dom
𝑂 ∈ dom
card) |
| 27 | 25, 26 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card) |
| 28 | | carddom2 10017 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ dom card ∧ dom 𝑂
∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom
𝑂)) |
| 29 | 23, 27, 28 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ((card‘ω) ⊆
(card‘dom 𝑂) ↔
ω ≼ dom 𝑂)) |
| 30 | 20, 29 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆
(card‘dom 𝑂)) |
| 31 | 13, 30 | eqsstrrid 4023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom
𝑂)) |
| 32 | | cardonle 9997 |
. . . . . . . . . . . 12
⊢ (dom
𝑂 ∈ On →
(card‘dom 𝑂) ⊆
dom 𝑂) |
| 33 | 25, 32 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂) |
| 34 | 31, 33 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂) |
| 35 | | sseq2 4010 |
. . . . . . . . . . . 12
⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂)) |
| 36 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂)) |
| 37 | 36 | f1oeq1d 6843 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
| 38 | | xpeq12 5710 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂)) |
| 39 | 38 | anidms 566 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂)) |
| 40 | 39 | f1oeq2d 6844 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏)) |
| 41 | | f1oeq3 6838 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
| 42 | 37, 40, 41 | 3bitrd 305 |
. . . . . . . . . . . 12
⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
| 43 | 35, 42 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ dom
𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂))) |
| 44 | | pwfseqlem5.n |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
| 46 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On) |
| 47 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 48 | | omex 9683 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ V |
| 49 | | ovex 7464 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ↑m 𝑛) ∈ V |
| 50 | 48, 49 | iunex 7993 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V |
| 51 | | f1dmex 7981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V) |
| 52 | 47, 50, 51 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V) |
| 53 | | pwexb 7786 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
| 54 | 52, 53 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V) |
| 55 | | simprl1 1219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴) |
| 56 | 4, 55 | sylan2b 594 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴) |
| 57 | | ssdomg 9040 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴)) |
| 58 | 54, 56, 57 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴) |
| 59 | | canth2g 9171 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
| 60 | | sdomdom 9020 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
| 61 | 54, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴) |
| 62 | | domtr 9047 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴) |
| 63 | 58, 61, 62 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴) |
| 64 | | endomtr 9052 |
. . . . . . . . . . . . 13
⊢ ((dom
𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴) |
| 65 | 17, 63, 64 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴) |
| 66 | | elharval 9601 |
. . . . . . . . . . . 12
⊢ (dom
𝑂 ∈
(har‘𝒫 𝐴)
↔ (dom 𝑂 ∈ On
∧ dom 𝑂 ≼
𝒫 𝐴)) |
| 67 | 46, 65, 66 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴)) |
| 68 | 43, 45, 67 | rspcdva 3623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
| 69 | 34, 68 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂) |
| 70 | | f1oco 6871 |
. . . . . . . . 9
⊢ ((𝑂:dom 𝑂–1-1-onto→𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡) |
| 71 | 12, 69, 70 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡) |
| 72 | | f1of 6848 |
. . . . . . . . . . . . . . 15
⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡) |
| 73 | 12, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡) |
| 74 | 73 | feqmptd 6977 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢))) |
| 75 | 74 | f1oeq1d 6843 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)) |
| 76 | 12, 75 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡) |
| 77 | 73 | feqmptd 6977 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣))) |
| 78 | 77 | f1oeq1d 6843 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)) |
| 79 | 12, 78 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡) |
| 80 | 76, 79 | xpf1o 9179 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
| 81 | | pwfseqlem5.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) |
| 82 | | f1oeq1 6836 |
. . . . . . . . . . 11
⊢ (𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) → (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))) |
| 83 | 81, 82 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
| 84 | 80, 83 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
| 85 | | f1ocnv 6860 |
. . . . . . . . 9
⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) |
| 86 | 84, 85 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) |
| 87 | | f1oco 6871 |
. . . . . . . 8
⊢ (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡 ∧ ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
| 88 | 71, 86, 87 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
| 89 | | pwfseqlem5.p |
. . . . . . . 8
⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) |
| 90 | | f1oeq1 6836 |
. . . . . . . 8
⊢ (𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) → (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)) |
| 91 | 89, 90 | ax-mp 5 |
. . . . . . 7
⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
| 92 | 88, 91 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡) |
| 93 | | f1of1 6847 |
. . . . . 6
⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡) |
| 94 | 92, 93 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡) |
| 95 | | f1of1 6847 |
. . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡) |
| 96 | 12, 95 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡) |
| 97 | | f1ssres 6811 |
. . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡) |
| 98 | 96, 34, 97 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡) |
| 99 | | f1f1orn 6859 |
. . . . . . . . . . 11
⊢ ((𝑂 ↾
ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω)) |
| 100 | 98, 99 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω)) |
| 101 | 73, 34 | feqresmpt 6978 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥))) |
| 102 | 101 | f1oeq1d 6843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω))) |
| 103 | 100, 102 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω)) |
| 104 | | mptresid 6069 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝑡) = (𝑦 ∈ 𝑡 ↦ 𝑦) |
| 105 | 104 | eqcomi 2746 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) |
| 106 | | f1oi 6886 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝑡):𝑡–1-1-onto→𝑡 |
| 107 | | f1oeq1 6836 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡)) |
| 108 | 106, 107 | mpbiri 258 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡) |
| 109 | 105, 108 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡) |
| 110 | 103, 109 | xpf1o 9179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
| 111 | | pwfseqlem5.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) |
| 112 | | f1oeq1 6836 |
. . . . . . . . 9
⊢ (𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) → (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡))) |
| 113 | 111, 112 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
| 114 | 110, 113 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
| 115 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡)) |
| 116 | 114, 115 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡)) |
| 117 | | f1f 6804 |
. . . . . . 7
⊢ ((𝑂 ↾
ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡) |
| 118 | | frn 6743 |
. . . . . . 7
⊢ ((𝑂 ↾
ω):ω⟶𝑡
→ ran (𝑂 ↾
ω) ⊆ 𝑡) |
| 119 | | xpss1 5704 |
. . . . . . 7
⊢ (ran
(𝑂 ↾ ω) ⊆
𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) |
| 120 | 98, 117, 118, 119 | 4syl 19 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) |
| 121 | | f1ss 6809 |
. . . . . 6
⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) |
| 122 | 116, 120,
121 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) |
| 123 | | f1co 6815 |
. . . . 5
⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡) |
| 124 | 94, 122, 123 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡) |
| 125 | 5 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V) |
| 126 | | peano1 7910 |
. . . . . . . 8
⊢ ∅
∈ ω |
| 127 | 126 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ∅ ∈
ω) |
| 128 | 34, 127 | sseldd 3984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂) |
| 129 | 73, 128 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡) |
| 130 | | pwfseqlem5.s |
. . . . 5
⊢ 𝑆 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {〈∅, (𝑂‘∅)〉}) |
| 131 | | pwfseqlem5.q |
. . . . 5
⊢ 𝑄 = (𝑦 ∈ ∪
𝑛 ∈ ω (𝑡 ↑m 𝑛) ↦ 〈dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)〉) |
| 132 | 125, 129,
92, 130, 131 | fseqenlem2 10065 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→(ω × 𝑡)) |
| 133 | | f1co 6815 |
. . . 4
⊢ (((𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡 ∧ 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→(ω × 𝑡)) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡) |
| 134 | 124, 132,
133 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡) |
| 135 | | pwfseqlem5.k |
. . . 4
⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) |
| 136 | | f1eq1 6799 |
. . . 4
⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡)) |
| 137 | 135, 136 | ax-mp 5 |
. . 3
⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡) |
| 138 | 134, 137 | sylibr 234 |
. 2
⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛)–1-1→𝑡) |
| 139 | | eqid 2737 |
. 2
⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))}) |
| 140 | | eqid 2737 |
. 2
⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) |
| 141 | | eqid 2737 |
. . 3
⊢
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} |
| 142 | 141 | fpwwe2cbv 10670 |
. 2
⊢
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))} |
| 143 | | eqid 2737 |
. 2
⊢ ∪ dom {〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = ∪ dom
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} |
| 144 | 1, 2, 3, 4, 138, 139, 140, 142, 143 | pwfseqlem4 10702 |
1
⊢ ¬
𝜑 |