Step |
Hyp |
Ref |
Expression |
1 |
|
isexid2.1 |
⊢ 𝑋 = ran 𝐺 |
2 |
|
rngopidOLD |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 ) |
3 |
|
elin |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) ↔ ( 𝐺 ∈ Magma ∧ 𝐺 ∈ ExId ) ) |
4 |
|
eqid |
⊢ dom dom 𝐺 = dom dom 𝐺 |
5 |
4
|
isexid |
⊢ ( 𝐺 ∈ ExId → ( 𝐺 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
6 |
5
|
ibi |
⊢ ( 𝐺 ∈ ExId → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) |
7 |
6
|
a1d |
⊢ ( 𝐺 ∈ ExId → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐺 ∈ Magma ∧ 𝐺 ∈ ExId ) → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
9 |
3 8
|
sylbi |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
10 |
|
eqeq2 |
⊢ ( ran 𝐺 = dom dom 𝐺 → ( 𝑋 = ran 𝐺 ↔ 𝑋 = dom dom 𝐺 ) ) |
11 |
|
raleq |
⊢ ( ran 𝐺 = dom dom 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
12 |
11
|
rexeqbi1dv |
⊢ ( ran 𝐺 = dom dom 𝐺 → ( ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
13 |
10 12
|
imbi12d |
⊢ ( ran 𝐺 = dom dom 𝐺 → ( ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ↔ ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺 ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) ) |
14 |
9 13
|
syl5ibr |
⊢ ( ran 𝐺 = dom dom 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) ) |
15 |
2 14
|
mpcom |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
16 |
15
|
com12 |
⊢ ( 𝑋 = ran 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
17 |
|
raleq |
⊢ ( 𝑋 = ran 𝐺 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
18 |
17
|
rexeqbi1dv |
⊢ ( 𝑋 = ran 𝐺 → ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
19 |
16 18
|
sylibrd |
⊢ ( 𝑋 = ran 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) |
20 |
1 19
|
ax-mp |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) |