| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | exidres.3 | . . . . . 6
⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) | 
| 2 |  | resexg 6044 | . . . . . 6
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ (𝐺 ↾ (𝑌 × 𝑌)) ∈ V) | 
| 3 | 1, 2 | eqeltrid 2844 | . . . . 5
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐻 ∈
V) | 
| 4 |  | eqid 2736 | . . . . . 6
⊢ ran 𝐻 = ran 𝐻 | 
| 5 | 4 | gidval 30532 | . . . . 5
⊢ (𝐻 ∈ V →
(GId‘𝐻) =
(℩𝑢 ∈ ran
𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) | 
| 6 | 3, 5 | syl 17 | . . . 4
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ (GId‘𝐻) =
(℩𝑢 ∈ ran
𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) | 
| 7 | 6 | 3ad2ant1 1133 | . . 3
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (GId‘𝐻) = (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) | 
| 8 | 7 | adantr 480 | . 2
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) | 
| 9 |  | exidres.1 | . . . . . . 7
⊢ 𝑋 = ran 𝐺 | 
| 10 |  | exidres.2 | . . . . . . 7
⊢ 𝑈 = (GId‘𝐺) | 
| 11 | 9, 10, 1 | exidreslem 37885 | . . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) | 
| 12 | 11 | simprd 495 | . . . . 5
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) | 
| 13 | 12 | adantr 480 | . . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) | 
| 14 | 9, 10, 1 | exidres 37886 | . . . . 5
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝐻 ∈ ExId ) | 
| 15 |  | elin 3966 | . . . . . . 7
⊢ (𝐻 ∈ (Magma ∩ ExId )
↔ (𝐻 ∈ Magma
∧ 𝐻 ∈ ExId
)) | 
| 16 |  | rngopidOLD 37861 | . . . . . . 7
⊢ (𝐻 ∈ (Magma ∩ ExId )
→ ran 𝐻 = dom dom
𝐻) | 
| 17 | 15, 16 | sylbir 235 | . . . . . 6
⊢ ((𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) → ran 𝐻 = dom dom 𝐻) | 
| 18 | 17 | ancoms 458 | . . . . 5
⊢ ((𝐻 ∈ ExId ∧ 𝐻 ∈ Magma) → ran 𝐻 = dom dom 𝐻) | 
| 19 | 14, 18 | sylan 580 | . . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ran 𝐻 = dom dom 𝐻) | 
| 20 | 13, 19 | raleqtrrdv 3329 | . . 3
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) | 
| 21 | 11 | simpld 494 | . . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ dom dom 𝐻) | 
| 22 | 21 | adantr 480 | . . . . 5
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → 𝑈 ∈ dom dom 𝐻) | 
| 23 | 22, 19 | eleqtrrd 2843 | . . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → 𝑈 ∈ ran 𝐻) | 
| 24 | 4 | exidu1 37864 | . . . . . . 7
⊢ (𝐻 ∈ (Magma ∩ ExId )
→ ∃!𝑢 ∈ ran
𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | 
| 25 | 15, 24 | sylbir 235 | . . . . . 6
⊢ ((𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) →
∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | 
| 26 | 25 | ancoms 458 | . . . . 5
⊢ ((𝐻 ∈ ExId ∧ 𝐻 ∈ Magma) →
∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | 
| 27 | 14, 26 | sylan 580 | . . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | 
| 28 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑢 = 𝑈 → (𝑢𝐻𝑥) = (𝑈𝐻𝑥)) | 
| 29 | 28 | eqeq1d 2738 | . . . . . 6
⊢ (𝑢 = 𝑈 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑈𝐻𝑥) = 𝑥)) | 
| 30 | 29 | ovanraleqv 7456 | . . . . 5
⊢ (𝑢 = 𝑈 → (∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) | 
| 31 | 30 | riota2 7414 | . . . 4
⊢ ((𝑈 ∈ ran 𝐻 ∧ ∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) → (∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) = 𝑈)) | 
| 32 | 23, 27, 31 | syl2anc 584 | . . 3
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) = 𝑈)) | 
| 33 | 20, 32 | mpbid 232 | . 2
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) = 𝑈) | 
| 34 | 8, 33 | eqtrd 2776 | 1
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = 𝑈) |