Step |
Hyp |
Ref |
Expression |
1 |
|
exidres.1 |
⊢ 𝑋 = ran 𝐺 |
2 |
|
exidres.2 |
⊢ 𝑈 = ( GId ‘ 𝐺 ) |
3 |
|
exidres.3 |
⊢ 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) |
4 |
|
resexg |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∈ V ) |
5 |
3 4
|
eqeltrid |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐻 ∈ V ) |
6 |
|
eqid |
⊢ ran 𝐻 = ran 𝐻 |
7 |
6
|
gidval |
⊢ ( 𝐻 ∈ V → ( GId ‘ 𝐻 ) = ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
8 |
5 7
|
syl |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( GId ‘ 𝐻 ) = ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
9 |
8
|
3ad2ant1 |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( GId ‘ 𝐻 ) = ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
10 |
9
|
adantr |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ( GId ‘ 𝐻 ) = ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
11 |
1 2 3
|
exidreslem |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) ) |
12 |
11
|
simprd |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) |
14 |
1 2 3
|
exidres |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝐻 ∈ ExId ) |
15 |
|
elin |
⊢ ( 𝐻 ∈ ( Magma ∩ ExId ) ↔ ( 𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) ) |
16 |
|
rngopidOLD |
⊢ ( 𝐻 ∈ ( Magma ∩ ExId ) → ran 𝐻 = dom dom 𝐻 ) |
17 |
15 16
|
sylbir |
⊢ ( ( 𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) → ran 𝐻 = dom dom 𝐻 ) |
18 |
17
|
ancoms |
⊢ ( ( 𝐻 ∈ ExId ∧ 𝐻 ∈ Magma ) → ran 𝐻 = dom dom 𝐻 ) |
19 |
14 18
|
sylan |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ran 𝐻 = dom dom 𝐻 ) |
20 |
19
|
raleqdv |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) ) |
21 |
13 20
|
mpbird |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) |
22 |
11
|
simpld |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝑈 ∈ dom dom 𝐻 ) |
23 |
22
|
adantr |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → 𝑈 ∈ dom dom 𝐻 ) |
24 |
23 19
|
eleqtrrd |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → 𝑈 ∈ ran 𝐻 ) |
25 |
6
|
exidu1 |
⊢ ( 𝐻 ∈ ( Magma ∩ ExId ) → ∃! 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) |
26 |
15 25
|
sylbir |
⊢ ( ( 𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) → ∃! 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) |
27 |
26
|
ancoms |
⊢ ( ( 𝐻 ∈ ExId ∧ 𝐻 ∈ Magma ) → ∃! 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) |
28 |
14 27
|
sylan |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ∃! 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) |
29 |
|
oveq1 |
⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐻 𝑥 ) = ( 𝑈 𝐻 𝑥 ) ) |
30 |
29
|
eqeq1d |
⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐻 𝑥 ) = 𝑥 ) ) |
31 |
30
|
ovanraleqv |
⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) ) |
32 |
31
|
riota2 |
⊢ ( ( 𝑈 ∈ ran 𝐻 ∧ ∃! 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) = 𝑈 ) ) |
33 |
24 28 32
|
syl2anc |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ( ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) = 𝑈 ) ) |
34 |
21 33
|
mpbid |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ( ℩ 𝑢 ∈ ran 𝐻 ∀ 𝑥 ∈ ran 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) = 𝑈 ) |
35 |
10 34
|
eqtrd |
⊢ ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) ∧ 𝐻 ∈ Magma ) → ( GId ‘ 𝐻 ) = 𝑈 ) |