| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1 2829 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵)) | 
| 2 |  | eleq1 2829 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝑦 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵)) | 
| 3 | 1, 2 | bi2anan9 638 | . . . . 5
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))) | 
| 4 |  | simpl 482 | . . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑥 = 𝑋) | 
| 5 | 4 | breq2d 5155 | . . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ( 0 < 𝑥 ↔ 0 < 𝑋)) | 
| 6 | 4 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝑛 · 𝑥) = (𝑛 · 𝑋)) | 
| 7 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) | 
| 8 | 6, 7 | breq12d 5156 | . . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑛 · 𝑥) < 𝑦 ↔ (𝑛 · 𝑋) < 𝑌)) | 
| 9 | 8 | ralbidv 3178 | . . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦 ↔ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌)) | 
| 10 | 5, 9 | anbi12d 632 | . . . . 5
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦) ↔ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌))) | 
| 11 | 3, 10 | anbi12d 632 | . . . 4
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦)) ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌)))) | 
| 12 |  | eqid 2737 | . . . 4
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))} | 
| 13 | 11, 12 | brabga 5539 | . . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))}𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌)))) | 
| 14 | 13 | 3adant1 1131 | . 2
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))}𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌)))) | 
| 15 |  | elex 3501 | . . . . 5
⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ V) | 
| 16 | 15 | 3ad2ant1 1134 | . . . 4
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑊 ∈ V) | 
| 17 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) | 
| 18 |  | inftm.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑊) | 
| 19 | 17, 18 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) | 
| 20 | 19 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (Base‘𝑤) ↔ 𝑥 ∈ 𝐵)) | 
| 21 | 19 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑦 ∈ (Base‘𝑤) ↔ 𝑦 ∈ 𝐵)) | 
| 22 | 20, 21 | anbi12d 632 | . . . . . . 7
⊢ (𝑤 = 𝑊 → ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) | 
| 23 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) | 
| 24 |  | inftm.0 | . . . . . . . . . 10
⊢  0 =
(0g‘𝑊) | 
| 25 | 23, 24 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 ) | 
| 26 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (lt‘𝑤) = (lt‘𝑊)) | 
| 27 |  | inftm.l | . . . . . . . . . 10
⊢  < =
(lt‘𝑊) | 
| 28 | 26, 27 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (lt‘𝑤) = < ) | 
| 29 |  | eqidd 2738 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) | 
| 30 | 25, 28, 29 | breq123d 5157 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → ((0g‘𝑤)(lt‘𝑤)𝑥 ↔ 0 < 𝑥)) | 
| 31 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (.g‘𝑤) = (.g‘𝑊)) | 
| 32 |  | inftm.x | . . . . . . . . . . . 12
⊢  · =
(.g‘𝑊) | 
| 33 | 31, 32 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (.g‘𝑤) = · ) | 
| 34 | 33 | oveqd 7448 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑛(.g‘𝑤)𝑥) = (𝑛 · 𝑥)) | 
| 35 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → 𝑦 = 𝑦) | 
| 36 | 34, 28, 35 | breq123d 5157 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦 ↔ (𝑛 · 𝑥) < 𝑦)) | 
| 37 | 36 | ralbidv 3178 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦 ↔ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦)) | 
| 38 | 30, 37 | anbi12d 632 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦) ↔ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))) | 
| 39 | 22, 38 | anbi12d 632 | . . . . . 6
⊢ (𝑤 = 𝑊 → (((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦)))) | 
| 40 | 39 | opabbidv 5209 | . . . . 5
⊢ (𝑤 = 𝑊 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))}) | 
| 41 |  | df-inftm 33185 | . . . . 5
⊢ ⋘
= (𝑤 ∈ V ↦
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))}) | 
| 42 | 18 | fvexi 6920 | . . . . . . 7
⊢ 𝐵 ∈ V | 
| 43 | 42, 42 | xpex 7773 | . . . . . 6
⊢ (𝐵 × 𝐵) ∈ V | 
| 44 |  | opabssxp 5778 | . . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))} ⊆ (𝐵 × 𝐵) | 
| 45 | 43, 44 | ssexi 5322 | . . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))} ∈ V | 
| 46 | 40, 41, 45 | fvmpt 7016 | . . . 4
⊢ (𝑊 ∈ V →
(⋘‘𝑊) =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))}) | 
| 47 | 16, 46 | syl 17 | . . 3
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⋘‘𝑊) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))}) | 
| 48 | 47 | breqd 5154 | . 2
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(⋘‘𝑊)𝑌 ↔ 𝑋{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))}𝑌)) | 
| 49 |  | 3simpc 1151 | . . 3
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | 
| 50 | 49 | biantrurd 532 | . 2
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌) ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌)))) | 
| 51 | 14, 48, 50 | 3bitr4d 311 | 1
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(⋘‘𝑊)𝑌 ↔ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌))) |