Step |
Hyp |
Ref |
Expression |
1 |
|
ecopopr.1 |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 〈 𝑧 , 𝑤 〉 ∧ 𝑦 = 〈 𝑣 , 𝑢 〉 ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) } |
2 |
|
ecopopr.com |
⊢ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) |
3 |
|
ecopopr.cl |
⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
4 |
|
ecopopr.ass |
⊢ ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) |
5 |
|
ecopopr.can |
⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑧 ) → 𝑦 = 𝑧 ) ) |
6 |
1
|
relopabiv |
⊢ Rel ∼ |
7 |
1 2
|
ecopovsym |
⊢ ( 𝑓 ∼ 𝑔 → 𝑔 ∼ 𝑓 ) |
8 |
1 2 3 4 5
|
ecopovtrn |
⊢ ( ( 𝑓 ∼ 𝑔 ∧ 𝑔 ∼ ℎ ) → 𝑓 ∼ ℎ ) |
9 |
|
vex |
⊢ 𝑔 ∈ V |
10 |
|
vex |
⊢ ℎ ∈ V |
11 |
9 10 2
|
caovcom |
⊢ ( 𝑔 + ℎ ) = ( ℎ + 𝑔 ) |
12 |
1
|
ecopoveq |
⊢ ( ( ( 𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆 ) ∧ ( 𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆 ) ) → ( 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 ↔ ( 𝑔 + ℎ ) = ( ℎ + 𝑔 ) ) ) |
13 |
11 12
|
mpbiri |
⊢ ( ( ( 𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆 ) ∧ ( 𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆 ) ) → 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 ) |
14 |
13
|
anidms |
⊢ ( ( 𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆 ) → 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 ) |
15 |
14
|
rgen2 |
⊢ ∀ 𝑔 ∈ 𝑆 ∀ ℎ ∈ 𝑆 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 |
16 |
|
breq12 |
⊢ ( ( 𝑓 = 〈 𝑔 , ℎ 〉 ∧ 𝑓 = 〈 𝑔 , ℎ 〉 ) → ( 𝑓 ∼ 𝑓 ↔ 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 ) ) |
17 |
16
|
anidms |
⊢ ( 𝑓 = 〈 𝑔 , ℎ 〉 → ( 𝑓 ∼ 𝑓 ↔ 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 ) ) |
18 |
17
|
ralxp |
⊢ ( ∀ 𝑓 ∈ ( 𝑆 × 𝑆 ) 𝑓 ∼ 𝑓 ↔ ∀ 𝑔 ∈ 𝑆 ∀ ℎ ∈ 𝑆 〈 𝑔 , ℎ 〉 ∼ 〈 𝑔 , ℎ 〉 ) |
19 |
15 18
|
mpbir |
⊢ ∀ 𝑓 ∈ ( 𝑆 × 𝑆 ) 𝑓 ∼ 𝑓 |
20 |
19
|
rspec |
⊢ ( 𝑓 ∈ ( 𝑆 × 𝑆 ) → 𝑓 ∼ 𝑓 ) |
21 |
|
opabssxp |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 〈 𝑧 , 𝑤 〉 ∧ 𝑦 = 〈 𝑣 , 𝑢 〉 ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) } ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) |
22 |
1 21
|
eqsstri |
⊢ ∼ ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) |
23 |
22
|
ssbri |
⊢ ( 𝑓 ∼ 𝑓 → 𝑓 ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) 𝑓 ) |
24 |
|
brxp |
⊢ ( 𝑓 ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) 𝑓 ↔ ( 𝑓 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 × 𝑆 ) ) ) |
25 |
24
|
simplbi |
⊢ ( 𝑓 ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) ) 𝑓 → 𝑓 ∈ ( 𝑆 × 𝑆 ) ) |
26 |
23 25
|
syl |
⊢ ( 𝑓 ∼ 𝑓 → 𝑓 ∈ ( 𝑆 × 𝑆 ) ) |
27 |
20 26
|
impbii |
⊢ ( 𝑓 ∈ ( 𝑆 × 𝑆 ) ↔ 𝑓 ∼ 𝑓 ) |
28 |
6 7 8 27
|
iseri |
⊢ ∼ Er ( 𝑆 × 𝑆 ) |