Proof of Theorem exidreslem
| Step | Hyp | Ref
| Expression |
| 1 | | exidres.3 |
. . . . . . . 8
⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) |
| 2 | 1 | dmeqi 5915 |
. . . . . . 7
⊢ dom 𝐻 = dom (𝐺 ↾ (𝑌 × 𝑌)) |
| 3 | | xpss12 5700 |
. . . . . . . . . . 11
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑌 ⊆ 𝑋) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑋)) |
| 4 | 3 | anidms 566 |
. . . . . . . . . 10
⊢ (𝑌 ⊆ 𝑋 → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑋)) |
| 5 | | exidres.1 |
. . . . . . . . . . . . 13
⊢ 𝑋 = ran 𝐺 |
| 6 | 5 | opidon2OLD 37861 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐺:(𝑋 × 𝑋)–onto→𝑋) |
| 7 | | fof 6820 |
. . . . . . . . . . . 12
⊢ (𝐺:(𝑋 × 𝑋)–onto→𝑋 → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
| 8 | | fdm 6745 |
. . . . . . . . . . . 12
⊢ (𝐺:(𝑋 × 𝑋)⟶𝑋 → dom 𝐺 = (𝑋 × 𝑋)) |
| 9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ dom 𝐺 = (𝑋 × 𝑋)) |
| 10 | 9 | sseq2d 4016 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ ((𝑌 × 𝑌) ⊆ dom 𝐺 ↔ (𝑌 × 𝑌) ⊆ (𝑋 × 𝑋))) |
| 11 | 4, 10 | imbitrrid 246 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ (𝑌 ⊆ 𝑋 → (𝑌 × 𝑌) ⊆ dom 𝐺)) |
| 12 | 11 | imp 406 |
. . . . . . . 8
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) → (𝑌 × 𝑌) ⊆ dom 𝐺) |
| 13 | | ssdmres 6031 |
. . . . . . . 8
⊢ ((𝑌 × 𝑌) ⊆ dom 𝐺 ↔ dom (𝐺 ↾ (𝑌 × 𝑌)) = (𝑌 × 𝑌)) |
| 14 | 12, 13 | sylib 218 |
. . . . . . 7
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) → dom (𝐺 ↾ (𝑌 × 𝑌)) = (𝑌 × 𝑌)) |
| 15 | 2, 14 | eqtrid 2789 |
. . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) → dom 𝐻 = (𝑌 × 𝑌)) |
| 16 | 15 | dmeqd 5916 |
. . . . 5
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) → dom dom 𝐻 = dom (𝑌 × 𝑌)) |
| 17 | | dmxpid 5941 |
. . . . 5
⊢ dom
(𝑌 × 𝑌) = 𝑌 |
| 18 | 16, 17 | eqtrdi 2793 |
. . . 4
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) → dom dom 𝐻 = 𝑌) |
| 19 | 18 | eleq2d 2827 |
. . 3
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) → (𝑈 ∈ dom dom 𝐻 ↔ 𝑈 ∈ 𝑌)) |
| 20 | 19 | biimp3ar 1472 |
. 2
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ dom dom 𝐻) |
| 21 | | ssel2 3978 |
. . . . . . . . . 10
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
| 22 | | exidres.2 |
. . . . . . . . . . 11
⊢ 𝑈 = (GId‘𝐺) |
| 23 | 5, 22 | cmpidelt 37866 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑥 ∈ 𝑋) → ((𝑈𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑈) = 𝑥)) |
| 24 | 21, 23 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ (𝑌 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑌)) → ((𝑈𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑈) = 𝑥)) |
| 25 | 24 | anassrs 467 |
. . . . . . . 8
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑌) → ((𝑈𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑈) = 𝑥)) |
| 26 | 25 | adantrl 716 |
. . . . . . 7
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) ∧ (𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌)) → ((𝑈𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑈) = 𝑥)) |
| 27 | 1 | oveqi 7444 |
. . . . . . . . . . 11
⊢ (𝑈𝐻𝑥) = (𝑈(𝐺 ↾ (𝑌 × 𝑌))𝑥) |
| 28 | | ovres 7599 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑈(𝐺 ↾ (𝑌 × 𝑌))𝑥) = (𝑈𝐺𝑥)) |
| 29 | 27, 28 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑈𝐻𝑥) = (𝑈𝐺𝑥)) |
| 30 | 29 | eqeq1d 2739 |
. . . . . . . . 9
⊢ ((𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → ((𝑈𝐻𝑥) = 𝑥 ↔ (𝑈𝐺𝑥) = 𝑥)) |
| 31 | 1 | oveqi 7444 |
. . . . . . . . . . . 12
⊢ (𝑥𝐻𝑈) = (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑈) |
| 32 | | ovres 7599 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑈 ∈ 𝑌) → (𝑥(𝐺 ↾ (𝑌 × 𝑌))𝑈) = (𝑥𝐺𝑈)) |
| 33 | 31, 32 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑈 ∈ 𝑌) → (𝑥𝐻𝑈) = (𝑥𝐺𝑈)) |
| 34 | 33 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (𝑥𝐻𝑈) = (𝑥𝐺𝑈)) |
| 35 | 34 | eqeq1d 2739 |
. . . . . . . . 9
⊢ ((𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → ((𝑥𝐻𝑈) = 𝑥 ↔ (𝑥𝐺𝑈) = 𝑥)) |
| 36 | 30, 35 | anbi12d 632 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌) → (((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ ((𝑈𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑈) = 𝑥))) |
| 37 | 36 | adantl 481 |
. . . . . . 7
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) ∧ (𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌)) → (((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥) ↔ ((𝑈𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑈) = 𝑥))) |
| 38 | 26, 37 | mpbird 257 |
. . . . . 6
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) ∧ (𝑈 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌)) → ((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
| 39 | 38 | anassrs 467 |
. . . . 5
⊢ ((((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) ∧ 𝑈 ∈ 𝑌) ∧ 𝑥 ∈ 𝑌) → ((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
| 40 | 39 | ralrimiva 3146 |
. . . 4
⊢ (((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋) ∧ 𝑈 ∈ 𝑌) → ∀𝑥 ∈ 𝑌 ((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
| 41 | 40 | 3impa 1110 |
. . 3
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → ∀𝑥 ∈ 𝑌 ((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
| 42 | 12 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑌 × 𝑌) ⊆ dom 𝐺) |
| 43 | 42, 13 | sylib 218 |
. . . . . 6
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → dom (𝐺 ↾ (𝑌 × 𝑌)) = (𝑌 × 𝑌)) |
| 44 | 2, 43 | eqtrid 2789 |
. . . . 5
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → dom 𝐻 = (𝑌 × 𝑌)) |
| 45 | 44 | dmeqd 5916 |
. . . 4
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → dom dom 𝐻 = dom (𝑌 × 𝑌)) |
| 46 | 45, 17 | eqtrdi 2793 |
. . 3
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → dom dom 𝐻 = 𝑌) |
| 47 | 41, 46 | raleqtrrdv 3330 |
. 2
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)) |
| 48 | 20, 47 | jca 511 |
1
⊢ ((𝐺 ∈ (Magma ∩ ExId )
∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) |