Step |
Hyp |
Ref |
Expression |
1 |
|
opidon2OLD.1 |
⊢ 𝑋 = ran 𝐺 |
2 |
|
eqid |
⊢ dom dom 𝐺 = dom dom 𝐺 |
3 |
2
|
opidonOLD |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ) |
4 |
|
forn |
⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → ran 𝐺 = dom dom 𝐺 ) |
5 |
1 4
|
eqtr2id |
⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → dom dom 𝐺 = 𝑋 ) |
6 |
|
xpeq12 |
⊢ ( ( dom dom 𝐺 = 𝑋 ∧ dom dom 𝐺 = 𝑋 ) → ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) ) |
7 |
6
|
anidms |
⊢ ( dom dom 𝐺 = 𝑋 → ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) ) |
8 |
|
foeq2 |
⊢ ( ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ) ) |
9 |
7 8
|
syl |
⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ) ) |
10 |
|
foeq3 |
⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) ) |
11 |
9 10
|
bitrd |
⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) ) |
12 |
11
|
biimpd |
⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) ) |
13 |
5 12
|
mpcom |
⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) |
14 |
3 13
|
syl |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) |