Step | Hyp | Ref
| Expression |
1 | | exidres.3 |
. . . . . 6
⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) |
2 | | resexg 5442 |
. . . . . 6
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ (𝐺 ↾ (𝑌 × 𝑌)) ∈ V) |
3 | 1, 2 | syl5eqel 2705 |
. . . . 5
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐻 ∈
V) |
4 | | eqid 2622 |
. . . . . 6
⊢ ran 𝐻 = ran 𝐻 |
5 | 4 | gidval 27366 |
. . . . 5
⊢ (𝐻 ∈ V →
(GId‘𝐻) =
(℩𝑢 ∈ ran
𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ (GId‘𝐻) =
(℩𝑢 ∈ ran
𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) |
7 | 6 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (GId‘𝐻) = (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) |
8 | 7 | adantr 481 |
. 2
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))) |
9 | | exidres.1 |
. . . . . . 7
⊢ 𝑋 = ran 𝐺 |
10 | | exidres.2 |
. . . . . . 7
⊢ 𝑈 = (GId‘𝐺) |
11 | 9, 10, 1 | exidreslem 33676 |
. . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) |
12 | 11 | simprd 479 |
. . . . 5
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
13 | 12 | adantr 481 |
. . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
14 | 9, 10, 1 | exidres 33677 |
. . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝐻 ∈ ExId ) |
15 | | elin 3796 |
. . . . . . . 8
⊢ (𝐻 ∈ (Magma ∩ ExId )
↔ (𝐻 ∈ Magma
∧ 𝐻 ∈ ExId
)) |
16 | | rngopidOLD 33652 |
. . . . . . . 8
⊢ (𝐻 ∈ (Magma ∩ ExId )
→ ran 𝐻 = dom dom
𝐻) |
17 | 15, 16 | sylbir 225 |
. . . . . . 7
⊢ ((𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) → ran 𝐻 = dom dom 𝐻) |
18 | 17 | ancoms 469 |
. . . . . 6
⊢ ((𝐻 ∈ ExId ∧ 𝐻 ∈ Magma) → ran 𝐻 = dom dom 𝐻) |
19 | 14, 18 | sylan 488 |
. . . . 5
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ran 𝐻 = dom dom 𝐻) |
20 | 19 | raleqdv 3144 |
. . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) |
21 | 13, 20 | mpbird 247 |
. . 3
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
22 | 11 | simpld 475 |
. . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ dom dom 𝐻) |
23 | 22 | adantr 481 |
. . . . 5
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → 𝑈 ∈ dom dom 𝐻) |
24 | 23, 19 | eleqtrrd 2704 |
. . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → 𝑈 ∈ ran 𝐻) |
25 | 4 | exidu1 33655 |
. . . . . . 7
⊢ (𝐻 ∈ (Magma ∩ ExId )
→ ∃!𝑢 ∈ ran
𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |
26 | 15, 25 | sylbir 225 |
. . . . . 6
⊢ ((𝐻 ∈ Magma ∧ 𝐻 ∈ ExId ) →
∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |
27 | 26 | ancoms 469 |
. . . . 5
⊢ ((𝐻 ∈ ExId ∧ 𝐻 ∈ Magma) →
∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |
28 | 14, 27 | sylan 488 |
. . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → ∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |
29 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑢 = 𝑈 → (𝑢𝐻𝑥) = (𝑈𝐻𝑥)) |
30 | 29 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑈𝐻𝑥) = 𝑥)) |
31 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑢 = 𝑈 → (𝑥𝐻𝑢) = (𝑥𝐻𝑈)) |
32 | 31 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → ((𝑥𝐻𝑢) = 𝑥 ↔ (𝑥𝐻𝑈) = 𝑥)) |
33 | 30, 32 | anbi12d 747 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) |
34 | 33 | ralbidv 2986 |
. . . . 5
⊢ (𝑢 = 𝑈 → (∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) |
35 | 34 | riota2 6633 |
. . . 4
⊢ ((𝑈 ∈ ran 𝐻 ∧ ∃!𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) → (∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) = 𝑈)) |
36 | 24, 28, 35 | syl2anc 693 |
. . 3
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (∀𝑥 ∈ ran 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) = 𝑈)) |
37 | 21, 36 | mpbid 222 |
. 2
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (℩𝑢 ∈ ran 𝐻∀𝑥 ∈ ran 𝐻((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) = 𝑈) |
38 | 8, 37 | eqtrd 2656 |
1
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = 𝑈) |