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 3176 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
6 | | simprl3 1101 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑟 We 𝑡) |
7 | 4, 6 | sylan2b 491 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑟 We 𝑡) |
8 | | pwfseqlem5.o |
. . . . . . . . . . . 12
⊢ 𝑂 = OrdIso(𝑟, 𝑡) |
9 | 8 | oiiso 8325 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡)) |
10 | 5, 7, 9 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡)) |
11 | | isof1o 6473 |
. . . . . . . . . 10
⊢ (𝑂 Isom E , 𝑟 (dom 𝑂, 𝑡) → 𝑂:dom 𝑂–1-1-onto→𝑡) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1-onto→𝑡) |
13 | 8 | oion 8324 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ V → dom 𝑂 ∈ On) |
14 | 5, 13 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom 𝑂 ∈ On |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ On) |
16 | 8 | oien 8326 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ V ∧ 𝑟 We 𝑡) → dom 𝑂 ≈ 𝑡) |
17 | 5, 7, 16 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≈ 𝑡) |
18 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
19 | | omex 8423 |
. . . . . . . . . . . . . . . . 17
⊢ ω
∈ V |
20 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ↑𝑚
𝑛) ∈
V |
21 | 19, 20 | iunex 7039 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ V |
22 | | f1dmex 7029 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ V) → 𝒫
𝐴 ∈
V) |
23 | 18, 21, 22 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝒫 𝐴 ∈ V) |
24 | | pwexb 6867 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
25 | 23, 24 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ V) |
26 | | simprl1 1099 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → 𝑡 ⊆ 𝐴) |
27 | 4, 26 | sylan2b 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ⊆ 𝐴) |
28 | | ssdomg 7887 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V → (𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴)) |
29 | 25, 27, 28 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝐴) |
30 | | canth2g 7999 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
31 | | sdomdom 7869 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
32 | 25, 30, 31 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ≼ 𝒫 𝐴) |
33 | | domtr 7895 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴) → 𝑡 ≼ 𝒫 𝐴) |
34 | 29, 32, 33 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≼ 𝒫 𝐴) |
35 | | endomtr 7900 |
. . . . . . . . . . . 12
⊢ ((dom
𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴) → dom 𝑂 ≼ 𝒫 𝐴) |
36 | 17, 34, 35 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ≼ 𝒫 𝐴) |
37 | | elharval 8351 |
. . . . . . . . . . 11
⊢ (dom
𝑂 ∈
(har‘𝒫 𝐴)
↔ (dom 𝑂 ∈ On
∧ dom 𝑂 ≼
𝒫 𝐴)) |
38 | 15, 36, 37 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ (har‘𝒫 𝐴)) |
39 | | pwfseqlem5.n |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
40 | 39 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
41 | | cardom 8695 |
. . . . . . . . . . . 12
⊢
(card‘ω) = ω |
42 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) → ω ≼ 𝑡) |
43 | 4, 42 | sylan2b 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ω ≼ 𝑡) |
44 | 17 | ensymd 7893 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ≈ dom 𝑂) |
45 | | domentr 7901 |
. . . . . . . . . . . . . 14
⊢ ((ω
≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂) → ω ≼ dom 𝑂) |
46 | 43, 44, 45 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ω ≼ dom 𝑂) |
47 | | omelon 8426 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
48 | | onenon 8658 |
. . . . . . . . . . . . . . 15
⊢ (ω
∈ On → ω ∈ dom card) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ω
∈ dom card |
50 | | onenon 8658 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑂 ∈ On → dom
𝑂 ∈ dom
card) |
51 | 14, 50 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → dom 𝑂 ∈ dom card) |
52 | | carddom2 8686 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ dom card ∧ dom 𝑂
∈ dom card) → ((card‘ω) ⊆ (card‘dom 𝑂) ↔ ω ≼ dom
𝑂)) |
53 | 49, 51, 52 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ((card‘ω) ⊆
(card‘dom 𝑂) ↔
ω ≼ dom 𝑂)) |
54 | 46, 53 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (card‘ω) ⊆
(card‘dom 𝑂)) |
55 | 41, 54 | syl5eqssr 3613 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → ω ⊆ (card‘dom
𝑂)) |
56 | | cardonle 8666 |
. . . . . . . . . . . 12
⊢ (dom
𝑂 ∈ On →
(card‘dom 𝑂) ⊆
dom 𝑂) |
57 | 15, 56 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (card‘dom 𝑂) ⊆ dom 𝑂) |
58 | 55, 57 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ω ⊆ dom 𝑂) |
59 | | sseq2 3590 |
. . . . . . . . . . . 12
⊢ (𝑏 = dom 𝑂 → (ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂)) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = dom 𝑂 → (𝑁‘𝑏) = (𝑁‘dom 𝑂)) |
61 | | f1oeq1 6040 |
. . . . . . . . . . . . . 14
⊢ ((𝑁‘𝑏) = (𝑁‘dom 𝑂) → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
63 | | xpeq12 5058 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂) → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂)) |
64 | 63 | anidms 675 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = dom 𝑂 → (𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂)) |
65 | | f1oeq2 6041 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 × 𝑏) = (dom 𝑂 × dom 𝑂) → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏)) |
67 | | f1oeq3 6042 |
. . . . . . . . . . . . 13
⊢ (𝑏 = dom 𝑂 → ((𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
68 | 62, 66, 67 | 3bitrd 293 |
. . . . . . . . . . . 12
⊢ (𝑏 = dom 𝑂 → ((𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂)) |
69 | 59, 68 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑏 = dom 𝑂 → ((ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ dom
𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂))) |
70 | 69 | rspcv 3278 |
. . . . . . . . . 10
⊢ (dom
𝑂 ∈
(har‘𝒫 𝐴)
→ (∀𝑏 ∈
(har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → (ω ⊆ dom
𝑂 → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂))) |
71 | 38, 40, 58, 70 | syl3c 64 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂) |
72 | | f1oco 6072 |
. . . . . . . . 9
⊢ ((𝑂:dom 𝑂–1-1-onto→𝑡 ∧ (𝑁‘dom 𝑂):(dom 𝑂 × dom 𝑂)–1-1-onto→dom
𝑂) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡) |
73 | 12, 71, 72 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡) |
74 | | f1of 6050 |
. . . . . . . . . . . . . . 15
⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂⟶𝑡) |
75 | 12, 74 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂⟶𝑡) |
76 | 75 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢))) |
77 | | f1oeq1 6040 |
. . . . . . . . . . . . 13
⊢ (𝑂 = (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡)) |
79 | 12, 78 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂 ↦ (𝑂‘𝑢)):dom 𝑂–1-1-onto→𝑡) |
80 | 75 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣))) |
81 | | f1oeq1 6040 |
. . . . . . . . . . . . 13
⊢ (𝑂 = (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑂:dom 𝑂–1-1-onto→𝑡 ↔ (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡)) |
83 | 12, 82 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑣 ∈ dom 𝑂 ↦ (𝑂‘𝑣)):dom 𝑂–1-1-onto→𝑡) |
84 | 79, 83 | xpf1o 8007 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
85 | | pwfseqlem5.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) |
86 | | f1oeq1 6040 |
. . . . . . . . . . 11
⊢ (𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) → (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡))) |
87 | 85, 86 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) ↔ (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉):(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
88 | 84, 87 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡)) |
89 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ (𝑇:(dom 𝑂 × dom 𝑂)–1-1-onto→(𝑡 × 𝑡) → ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) |
90 | 88, 89 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) |
91 | | f1oco 6072 |
. . . . . . . 8
⊢ (((𝑂 ∘ (𝑁‘dom 𝑂)):(dom 𝑂 × dom 𝑂)–1-1-onto→𝑡 ∧ ◡𝑇:(𝑡 × 𝑡)–1-1-onto→(dom
𝑂 × dom 𝑂)) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
92 | 73, 90, 91 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
93 | | pwfseqlem5.p |
. . . . . . . 8
⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) |
94 | | f1oeq1 6040 |
. . . . . . . 8
⊢ (𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) → (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡)) |
95 | 93, 94 | ax-mp 5 |
. . . . . . 7
⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 ↔ ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇):(𝑡 × 𝑡)–1-1-onto→𝑡) |
96 | 92, 95 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡) |
97 | | f1of1 6049 |
. . . . . 6
⊢ (𝑃:(𝑡 × 𝑡)–1-1-onto→𝑡 → 𝑃:(𝑡 × 𝑡)–1-1→𝑡) |
98 | 96, 97 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑃:(𝑡 × 𝑡)–1-1→𝑡) |
99 | | f1of1 6049 |
. . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→𝑡 → 𝑂:dom 𝑂–1-1→𝑡) |
100 | 12, 99 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑂:dom 𝑂–1-1→𝑡) |
101 | | f1ssres 6021 |
. . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂–1-1→𝑡 ∧ ω ⊆ dom 𝑂) → (𝑂 ↾ ω):ω–1-1→𝑡) |
102 | 100, 58, 101 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1→𝑡) |
103 | | f1f1orn 6061 |
. . . . . . . . . . 11
⊢ ((𝑂 ↾
ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω)) |
104 | 102, 103 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω)) |
105 | 75, 58 | feqresmpt 6160 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥))) |
106 | | f1oeq1 6040 |
. . . . . . . . . . 11
⊢ ((𝑂 ↾ ω) = (𝑥 ∈ ω ↦ (𝑂‘𝑥)) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω))) |
107 | 105, 106 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑂 ↾ ω):ω–1-1-onto→ran (𝑂 ↾ ω) ↔ (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω))) |
108 | 104, 107 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω ↦ (𝑂‘𝑥)):ω–1-1-onto→ran
(𝑂 ↾
ω)) |
109 | | mptresid 5375 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) |
110 | | f1oi 6086 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝑡):𝑡–1-1-onto→𝑡 |
111 | | f1oeq1 6040 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → ((𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡 ↔ ( I ↾ 𝑡):𝑡–1-1-onto→𝑡)) |
112 | 110, 111 | mpbiri 247 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑡 ↦ 𝑦) = ( I ↾ 𝑡) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡) |
113 | 109, 112 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑦 ∈ 𝑡 ↦ 𝑦):𝑡–1-1-onto→𝑡) |
114 | 108, 113 | xpf1o 8007 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
115 | | pwfseqlem5.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) |
116 | | f1oeq1 6040 |
. . . . . . . . 9
⊢ (𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) → (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡))) |
117 | 115, 116 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) ↔ (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉):(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
118 | 114, 117 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡)) |
119 | | f1of1 6049 |
. . . . . . 7
⊢ (𝐼:(ω × 𝑡)–1-1-onto→(ran
(𝑂 ↾ ω) ×
𝑡) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡)) |
120 | 118, 119 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡)) |
121 | | f1f 6014 |
. . . . . . 7
⊢ ((𝑂 ↾
ω):ω–1-1→𝑡 → (𝑂 ↾ ω):ω⟶𝑡) |
122 | | frn 5966 |
. . . . . . 7
⊢ ((𝑂 ↾
ω):ω⟶𝑡
→ ran (𝑂 ↾
ω) ⊆ 𝑡) |
123 | | xpss1 5151 |
. . . . . . 7
⊢ (ran
(𝑂 ↾ ω) ⊆
𝑡 → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) |
124 | 102, 121,
122, 123 | 4syl 19 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) |
125 | | f1ss 6019 |
. . . . . 6
⊢ ((𝐼:(ω × 𝑡)–1-1→(ran (𝑂 ↾ ω) × 𝑡) ∧ (ran (𝑂 ↾ ω) × 𝑡) ⊆ (𝑡 × 𝑡)) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) |
126 | 120, 124,
125 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) |
127 | | f1co 6023 |
. . . . 5
⊢ ((𝑃:(𝑡 × 𝑡)–1-1→𝑡 ∧ 𝐼:(ω × 𝑡)–1-1→(𝑡 × 𝑡)) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡) |
128 | 98, 126, 127 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡) |
129 | 5 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑡 ∈ V) |
130 | | peano1 6977 |
. . . . . . . 8
⊢ ∅
∈ ω |
131 | 130 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ∅ ∈
ω) |
132 | 58, 131 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ∅ ∈ dom 𝑂) |
133 | 75, 132 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑂‘∅) ∈ 𝑡) |
134 | | pwfseqlem5.s |
. . . . 5
⊢ 𝑆 =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ (𝑥 ∈ (𝑡 ↑𝑚 suc
𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {〈∅, (𝑂‘∅)〉}) |
135 | | pwfseqlem5.q |
. . . . 5
⊢ 𝑄 = (𝑦 ∈ ∪
𝑛 ∈ ω (𝑡 ↑𝑚
𝑛) ↦ 〈dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)〉) |
136 | 129, 133,
96, 134, 135 | fseqenlem2 8731 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→(ω × 𝑡)) |
137 | | f1co 6023 |
. . . 4
⊢ (((𝑃 ∘ 𝐼):(ω × 𝑡)–1-1→𝑡 ∧ 𝑄:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→(ω × 𝑡)) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
138 | 128, 136,
137 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
139 | | pwfseqlem5.k |
. . . 4
⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) |
140 | | f1eq1 6009 |
. . . 4
⊢ (𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) → (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡)) |
141 | 139, 140 | ax-mp 5 |
. . 3
⊢ (𝐾:∪ 𝑛 ∈ ω (𝑡 ↑𝑚 𝑛)–1-1→𝑡 ↔ ((𝑃 ∘ 𝐼) ∘ 𝑄):∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
142 | 138, 141 | sylibr 223 |
. 2
⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑡 ↑𝑚
𝑛)–1-1→𝑡) |
143 | | eqid 2610 |
. 2
⊢ (𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))}) = (𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))}) |
144 | | eqid 2610 |
. 2
⊢ (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) = (𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡}))) |
145 | | eqid 2610 |
. . 3
⊢
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} |
146 | 145 | fpwwe2cbv 9331 |
. 2
⊢
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑤](𝑤(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑠 ∩ (𝑤 × 𝑤))) = 𝑏))} |
147 | | eqid 2610 |
. 2
⊢ ∪ dom {〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} = ∪ dom
{〈𝑐, 𝑑〉 ∣ ((𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ (𝑐 × 𝑐)) ∧ (𝑑 We 𝑐 ∧ ∀𝑚 ∈ 𝑐 [(◡𝑑 “ {𝑚}) / 𝑗](𝑗(𝑡 ∈ V, 𝑟 ∈ V ↦ if(𝑡 ∈ Fin, (𝐻‘(card‘𝑡)), ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘∩
{𝑧 ∈ ω ∣
¬ ((𝐺‘{𝑖 ∈ 𝑡 ∣ ((◡𝐾‘𝑖) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ (◡𝐺‘(◡𝐾‘𝑖)))})‘𝑧) ∈ 𝑡})))(𝑑 ∩ (𝑗 × 𝑗))) = 𝑚))} |
148 | 1, 2, 3, 4, 142, 143, 144, 146, 147 | pwfseqlem4 9363 |
1
⊢ ¬
𝜑 |