Step | Hyp | Ref
| Expression |
1 | | pwfseqlem5.g |
. 2
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
2 | | pwfseqlem5.x |
. 2
⊢ (𝜑 → 𝑋 ⊆ 𝐴) |
3 | | pwfseqlem5.h |
. 2
⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) |
4 | | pwfseqlem5.ps |
. 2
⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) |
5 | | vex 3418 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
6 | | simprl3 1200 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡) |
7 | 4, 6 | sylan2b 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡) |
8 | | pwfseqlem5.o |
. . . . . . . . . . . 12
⊢ 𝑂 = OrdIso(𝑟, 𝑡) |
9 | 8 | oiiso 8796 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡)) |
10 | 5, 7, 9 | sylancr 578 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡)) |
11 | | isof1o 6899 |
. . . . . . . . . 10
⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡) |
13 | | cardom 9209 |
. . . . . . . . . . . 12
⊢
(card‘ω) = ω |
14 | | simprr 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡) |
15 | 4, 14 | sylan2b 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡) |
16 | 8 | oien 8797 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡) |
17 | 5, 7, 16 | sylancr 578 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡) |
18 | 17 | ensymd 8357 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂) |
19 | | domentr 8365 |
. . . . . . . . . . . . . 14
⊢ ((ω
≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂) |
20 | 15, 18, 19 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂) |
21 | | omelon 8903 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
22 | | onenon 9172 |
. . . . . . . . . . . . . . 15
⊢ (ω
∈ On → ω ∈ dom card) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ω
∈ dom card |
24 | 8 | oion 8795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ V → dom 𝑂 ∈ On) |
25 | 24 | elv 3420 |
. . . . . . . . . . . . . . 15
⊢ dom 𝑂 ∈ On |
26 | | onenon 9172 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑂 ∈ On → dom
𝑂 ∈ dom
card) |
27 | 25, 26 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card) |
28 | | carddom2 9200 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ dom card ∧ dom 𝑂
∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom
𝑂)) |
29 | 23, 27, 28 | sylancr 578 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ((card‘ω) ⊆
(card‘dom 𝑂) ↔
ω ≼ dom 𝑂)) |
30 | 20, 29 | mpbird 249 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆
(card‘dom 𝑂)) |
31 | 13, 30 | syl5eqssr 3906 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom
𝑂)) |
32 | | cardonle 9180 |
. . . . . . . . . . . 12
⊢ (dom
𝑂 ∈ On →
(card‘dom 𝑂) ⊆
dom 𝑂) |
33 | 25, 32 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂) |
34 | 31, 33 | sstrd 3868 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂) |
35 | | sseq2 3883 |
. . . . . . . . . . . 12
⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂)) |
36 | | fveq2 6499 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂)) |
37 | | f1oeq1 6433 |
. . . . . . . . . . . . . 14
⊢ ((𝑁‘𝑏) = (𝑁‘dom 𝑂) → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
39 | | xpeq12 5432 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂)) |
40 | 39 | anidms 559 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂)) |
41 | 40 | f1oeq2d 6440 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏)) |
42 | | f1oeq3 6435 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
43 | 38, 41, 42 | 3bitrd 297 |
. . . . . . . . . . . 12
⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
44 | 35, 43 | imbi12d 337 |
. . . . . . . . . . 11
⊢ (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ dom
𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂))) |
45 | | pwfseqlem5.n |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
46 | 45 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
47 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On) |
48 | 1 | adantr 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
49 | | omex 8900 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ V |
50 | | ovex 7008 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ↑𝑚
𝑛) ∈
V |
51 | 49, 50 | iunex 7481 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ V |
52 | | f1dmex 7470 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ V) → 𝒫
𝐴 ∈
V) |
53 | 48, 51, 52 | sylancl 577 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V) |
54 | | pwexb 7305 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
55 | 53, 54 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V) |
56 | | simprl1 1198 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴) |
57 | 4, 56 | sylan2b 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴) |
58 | | ssdomg 8352 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴)) |
59 | 55, 57, 58 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴) |
60 | | canth2g 8467 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
61 | | sdomdom 8334 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
62 | 55, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴) |
63 | | domtr 8359 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴) |
64 | 59, 62, 63 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴) |
65 | | endomtr 8364 |
. . . . . . . . . . . . 13
⊢ ((dom
𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴) |
66 | 17, 64, 65 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴) |
67 | | elharval 8822 |
. . . . . . . . . . . 12
⊢ (dom
𝑂 ∈
(har‘𝒫 𝐴)
↔ (dom 𝑂 ∈ On
∧ dom 𝑂 ≼
𝒫 𝐴)) |
68 | 47, 66, 67 | sylanbrc 575 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴)) |
69 | 44, 46, 68 | rspcdva 3541 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (ω ⊆ dom 𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
70 | 34, 69 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂) |
71 | | f1oco 6466 |
. . . . . . . . 9
⊢ ((𝑂:dom 𝑂–1-1-onto→𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡) |
72 | 12, 70, 71 | syl2anc 576 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡) |
73 | | f1of 6444 |
. . . . . . . . . . . . . . 15
⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡) |
74 | 12, 73 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡) |
75 | 74 | feqmptd 6562 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢))) |
76 | | f1oeq1 6433 |
. . . . . . . . . . . . 13
⊢ (𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)) |
78 | 12, 77 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡) |
79 | 74 | feqmptd 6562 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣))) |
80 | | f1oeq1 6433 |
. . . . . . . . . . . . 13
⊢ (𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)) |
82 | 12, 81 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡) |
83 | 78, 82 | xpf1o 8475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
84 | | pwfseqlem5.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) |
85 | | f1oeq1 6433 |
. . . . . . . . . . 11
⊢ (𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) → (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
87 | 83, 86 | sylibr 226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
88 | | f1ocnv 6456 |
. . . . . . . . 9
⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) |
89 | 87, 88 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) |
90 | | f1oco 6466 |
. . . . . . . 8
⊢ (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡 ∧ ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
91 | 72, 89, 90 | syl2anc 576 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
92 | | pwfseqlem5.p |
. . . . . . . 8
⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) |
93 | | f1oeq1 6433 |
. . . . . . . 8
⊢ (𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) → (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)) |
94 | 92, 93 | ax-mp 5 |
. . . . . . 7
⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
95 | 91, 94 | sylibr 226 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡) |
96 | | f1of1 6443 |
. . . . . 6
⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡) |
97 | 95, 96 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡) |
98 | | f1of1 6443 |
. . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡) |
99 | 12, 98 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡) |
100 | | f1ssres 6411 |
. . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡) |
101 | 99, 34, 100 | syl2anc 576 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡) |
102 | | f1f1orn 6455 |
. . . . . . . . . . 11
⊢ ((𝑂 ↾
ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω)) |
104 | 74, 34 | feqresmpt 6563 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥))) |
105 | | f1oeq1 6433 |
. . . . . . . . . . 11
⊢ ((𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω))) |
106 | 104, 105 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω))) |
107 | 103, 106 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω)) |
108 | | mptresid 5762 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) |
109 | | f1oi 6481 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝑡):𝑡–1-1-onto→𝑡 |
110 | | f1oeq1 6433 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡)) |
111 | 109, 110 | mpbiri 250 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡) |
112 | 108, 111 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡) |
113 | 107, 112 | xpf1o 8475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
114 | | pwfseqlem5.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) |
115 | | f1oeq1 6433 |
. . . . . . . . 9
⊢ (𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) → (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡))) |
116 | 114, 115 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
117 | 113, 116 | sylibr 226 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
118 | | f1of1 6443 |
. . . . . . 7
⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡)) |
119 | 117, 118 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡)) |
120 | | f1f 6404 |
. . . . . . 7
⊢ ((𝑂 ↾
ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡) |
121 | | frn 6350 |
. . . . . . 7
⊢ ((𝑂 ↾
ω):ω⟶𝑡
→ ran (𝑂 ↾
ω) ⊆ 𝑡) |
122 | | xpss1 5426 |
. . . . . . 7
⊢ (ran
(𝑂 ↾ ω) ⊆
𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) |
123 | 101, 120,
121, 122 | 4syl 19 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) |
124 | | f1ss 6409 |
. . . . . 6
⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) |
125 | 119, 123,
124 | syl2anc 576 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) |
126 | | f1co 6414 |
. . . . 5
⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡) |
127 | 97, 125, 126 | syl2anc 576 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡) |
128 | 5 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V) |
129 | | peano1 7416 |
. . . . . . . 8
⊢ ∅
∈ ω |
130 | 129 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ∅ ∈
ω) |
131 | 34, 130 | sseldd 3859 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂) |
132 | 74, 131 | ffvelrnd 6677 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡) |
133 | | pwfseqlem5.s |
. . . . 5
⊢ 𝑆 =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ (𝑥 ∈ (𝑡 ↑𝑚 suc
𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {〈∅, (𝑂‘∅)〉}) |
134 | | pwfseqlem5.q |
. . . . 5
⊢ 𝑄 = (𝑦 ∈ ∪
𝑛 ∈ ω (𝑡 ↑𝑚
𝑛) ↦ 〈dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)〉) |
135 | 128, 132,
95, 133, 134 | fseqenlem2 9245 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→(ω × 𝑡)) |
136 | | f1co 6414 |
. . . 4
⊢ (((𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡 ∧ 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→(ω × 𝑡)) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
137 | 127, 135,
136 | syl2anc 576 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
138 | | pwfseqlem5.k |
. . . 4
⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) |
139 | | f1eq1 6399 |
. . . 4
⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡)) |
140 | 138, 139 | ax-mp 5 |
. . 3
⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑𝑚 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
141 | 137, 140 | sylibr 226 |
. 2
⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
142 | | eqid 2778 |
. 2
⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))}) |
143 | | eqid 2778 |
. 2
⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) |
144 | | eqid 2778 |
. . 3
⊢
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} |
145 | 144 | fpwwe2cbv 9850 |
. 2
⊢
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))} |
146 | | eqid 2778 |
. 2
⊢ ∪ dom {〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = ∪ dom
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} |
147 | 1, 2, 3, 4, 141, 142, 143, 145, 146 | pwfseqlem4 9882 |
1
⊢ ¬
𝜑 |