Step | Hyp | Ref
| Expression |
1 | | elex 3450 |
. . 3
⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ V) |
2 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
3 | | inftm.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑊) |
4 | 2, 3 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) |
5 | 4 | eleq2d 2824 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘𝑤) ↔ 𝑥 ∈ 𝐵)) |
6 | 4 | eleq2d 2824 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑦 ∈ (Base‘𝑤) ↔ 𝑦 ∈ 𝐵)) |
7 | 5, 6 | anbi12d 631 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
8 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) |
9 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (lt‘𝑤) = (lt‘𝑊)) |
10 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) |
11 | 8, 9, 10 | breq123d 5088 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((0g‘𝑤)(lt‘𝑤)𝑥 ↔ (0g‘𝑊)(lt‘𝑊)𝑥)) |
12 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (.g‘𝑤) = (.g‘𝑊)) |
13 | 12 | oveqd 7292 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑛(.g‘𝑤)𝑥) = (𝑛(.g‘𝑊)𝑥)) |
14 | | eqidd 2739 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → 𝑦 = 𝑦) |
15 | 13, 9, 14 | breq123d 5088 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦 ↔ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦)) |
16 | 15 | ralbidv 3112 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦 ↔ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦)) |
17 | 11, 16 | anbi12d 631 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦) ↔ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦))) |
18 | 7, 17 | anbi12d 631 |
. . . . 5
⊢ (𝑤 = 𝑊 → (((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦)))) |
19 | 18 | opabbidv 5140 |
. . . 4
⊢ (𝑤 = 𝑊 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦))}) |
20 | | df-inftm 31432 |
. . . 4
⊢ ⋘
= (𝑤 ∈ V ↦
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))}) |
21 | 3 | fvexi 6788 |
. . . . . 6
⊢ 𝐵 ∈ V |
22 | 21, 21 | xpex 7603 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
23 | | opabssxp 5679 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦))} ⊆ (𝐵 × 𝐵) |
24 | 22, 23 | ssexi 5246 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦))} ∈ V |
25 | 19, 20, 24 | fvmpt 6875 |
. . 3
⊢ (𝑊 ∈ V →
(⋘‘𝑊) =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦))}) |
26 | 1, 25 | syl 17 |
. 2
⊢ (𝑊 ∈ 𝑉 → (⋘‘𝑊) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑊)𝑥)(lt‘𝑊)𝑦))}) |
27 | 26, 23 | eqsstrdi 3975 |
1
⊢ (𝑊 ∈ 𝑉 → (⋘‘𝑊) ⊆ (𝐵 × 𝐵)) |