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