Step |
Hyp |
Ref |
Expression |
1 |
|
exidres.1 |
⊢ 𝑋 = ran 𝐺 |
2 |
|
exidres.2 |
⊢ 𝑈 = ( GId ‘ 𝐺 ) |
3 |
|
exidres.3 |
⊢ 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) |
4 |
1 2 3
|
exidreslem |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) ) |
5 |
|
oveq1 |
⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐻 𝑥 ) = ( 𝑈 𝐻 𝑥 ) ) |
6 |
5
|
eqeq1d |
⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐻 𝑥 ) = 𝑥 ) ) |
7 |
6
|
ovanraleqv |
⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) ) |
8 |
7
|
rspcev |
⊢ ( ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) → ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) |
9 |
4 8
|
syl |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) |
10 |
|
resexg |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∈ V ) |
11 |
3 10
|
eqeltrid |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐻 ∈ V ) |
12 |
|
eqid |
⊢ dom dom 𝐻 = dom dom 𝐻 |
13 |
12
|
isexid |
⊢ ( 𝐻 ∈ V → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
14 |
11 13
|
syl |
⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) |
16 |
9 15
|
mpbird |
⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝐻 ∈ ExId ) |