Step | Hyp | Ref
| Expression |
1 | | feq1 6026 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑔:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
2 | 1 | exbidv 1850 |
. . . 4
⊢ (𝑔 = 𝐺 → (∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡 ↔ ∃𝑡 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
3 | | df-mgmOLD 33648 |
. . . 4
⊢ Magma =
{𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡} |
4 | 2, 3 | elab2g 3353 |
. . 3
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ ∃𝑡 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
5 | | f00 6087 |
. . . . . . . 8
⊢ (𝐺:(∅ ×
∅)⟶∅ ↔ (𝐺 = ∅ ∧ (∅ × ∅) =
∅)) |
6 | | dmeq 5324 |
. . . . . . . . . 10
⊢ (𝐺 = ∅ → dom 𝐺 = dom ∅) |
7 | | dmeq 5324 |
. . . . . . . . . . 11
⊢ (dom
𝐺 = dom ∅ → dom
dom 𝐺 = dom dom
∅) |
8 | | dm0 5339 |
. . . . . . . . . . . . 13
⊢ dom
∅ = ∅ |
9 | 8 | dmeqi 5325 |
. . . . . . . . . . . 12
⊢ dom dom
∅ = dom ∅ |
10 | 9, 8 | eqtri 2644 |
. . . . . . . . . . 11
⊢ dom dom
∅ = ∅ |
11 | 7, 10 | syl6req 2673 |
. . . . . . . . . 10
⊢ (dom
𝐺 = dom ∅ →
∅ = dom dom 𝐺) |
12 | 6, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝐺 = ∅ → ∅ = dom
dom 𝐺) |
13 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((𝐺 = ∅ ∧ (∅
× ∅) = ∅) → ∅ = dom dom 𝐺) |
14 | 5, 13 | sylbi 207 |
. . . . . . 7
⊢ (𝐺:(∅ ×
∅)⟶∅ → ∅ = dom dom 𝐺) |
15 | | xpeq12 5134 |
. . . . . . . . . 10
⊢ ((𝑡 = ∅ ∧ 𝑡 = ∅) → (𝑡 × 𝑡) = (∅ ×
∅)) |
16 | 15 | anidms 677 |
. . . . . . . . 9
⊢ (𝑡 = ∅ → (𝑡 × 𝑡) = (∅ ×
∅)) |
17 | | feq23 6029 |
. . . . . . . . 9
⊢ (((𝑡 × 𝑡) = (∅ × ∅) ∧ 𝑡 = ∅) → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(∅ ×
∅)⟶∅)) |
18 | 16, 17 | mpancom 703 |
. . . . . . . 8
⊢ (𝑡 = ∅ → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(∅ ×
∅)⟶∅)) |
19 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑡 = ∅ → (𝑡 = dom dom 𝐺 ↔ ∅ = dom dom 𝐺)) |
20 | 18, 19 | imbi12d 334 |
. . . . . . 7
⊢ (𝑡 = ∅ → ((𝐺:(𝑡 × 𝑡)⟶𝑡 → 𝑡 = dom dom 𝐺) ↔ (𝐺:(∅ × ∅)⟶∅
→ ∅ = dom dom 𝐺))) |
21 | 14, 20 | mpbiri 248 |
. . . . . 6
⊢ (𝑡 = ∅ → (𝐺:(𝑡 × 𝑡)⟶𝑡 → 𝑡 = dom dom 𝐺)) |
22 | | fdm 6051 |
. . . . . . . 8
⊢ (𝐺:(𝑡 × 𝑡)⟶𝑡 → dom 𝐺 = (𝑡 × 𝑡)) |
23 | | dmeq 5324 |
. . . . . . . 8
⊢ (dom
𝐺 = (𝑡 × 𝑡) → dom dom 𝐺 = dom (𝑡 × 𝑡)) |
24 | | df-ne 2795 |
. . . . . . . . . . . 12
⊢ (𝑡 ≠ ∅ ↔ ¬ 𝑡 = ∅) |
25 | | dmxp 5344 |
. . . . . . . . . . . 12
⊢ (𝑡 ≠ ∅ → dom (𝑡 × 𝑡) = 𝑡) |
26 | 24, 25 | sylbir 225 |
. . . . . . . . . . 11
⊢ (¬
𝑡 = ∅ → dom
(𝑡 × 𝑡) = 𝑡) |
27 | 26 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (¬
𝑡 = ∅ → (dom
(𝑡 × 𝑡) = dom dom 𝐺 ↔ 𝑡 = dom dom 𝐺)) |
28 | 27 | biimpcd 239 |
. . . . . . . . 9
⊢ (dom
(𝑡 × 𝑡) = dom dom 𝐺 → (¬ 𝑡 = ∅ → 𝑡 = dom dom 𝐺)) |
29 | 28 | eqcoms 2630 |
. . . . . . . 8
⊢ (dom dom
𝐺 = dom (𝑡 × 𝑡) → (¬ 𝑡 = ∅ → 𝑡 = dom dom 𝐺)) |
30 | 22, 23, 29 | 3syl 18 |
. . . . . . 7
⊢ (𝐺:(𝑡 × 𝑡)⟶𝑡 → (¬ 𝑡 = ∅ → 𝑡 = dom dom 𝐺)) |
31 | 30 | com12 32 |
. . . . . 6
⊢ (¬
𝑡 = ∅ → (𝐺:(𝑡 × 𝑡)⟶𝑡 → 𝑡 = dom dom 𝐺)) |
32 | 21, 31 | pm2.61i 176 |
. . . . 5
⊢ (𝐺:(𝑡 × 𝑡)⟶𝑡 → 𝑡 = dom dom 𝐺) |
33 | 32 | pm4.71ri 665 |
. . . 4
⊢ (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ (𝑡 = dom dom 𝐺 ∧ 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
34 | 33 | exbii 1774 |
. . 3
⊢
(∃𝑡 𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ ∃𝑡(𝑡 = dom dom 𝐺 ∧ 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
35 | 4, 34 | syl6bb 276 |
. 2
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ ∃𝑡(𝑡 = dom dom 𝐺 ∧ 𝐺:(𝑡 × 𝑡)⟶𝑡))) |
36 | | dmexg 7097 |
. . 3
⊢ (𝐺 ∈ 𝐴 → dom 𝐺 ∈ V) |
37 | | dmexg 7097 |
. . 3
⊢ (dom
𝐺 ∈ V → dom dom
𝐺 ∈
V) |
38 | | xpeq12 5134 |
. . . . . . 7
⊢ ((𝑡 = dom dom 𝐺 ∧ 𝑡 = dom dom 𝐺) → (𝑡 × 𝑡) = (dom dom 𝐺 × dom dom 𝐺)) |
39 | 38 | anidms 677 |
. . . . . 6
⊢ (𝑡 = dom dom 𝐺 → (𝑡 × 𝑡) = (dom dom 𝐺 × dom dom 𝐺)) |
40 | | feq23 6029 |
. . . . . 6
⊢ (((𝑡 × 𝑡) = (dom dom 𝐺 × dom dom 𝐺) ∧ 𝑡 = dom dom 𝐺) → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(dom dom 𝐺 × dom dom 𝐺)⟶dom dom 𝐺)) |
41 | 39, 40 | mpancom 703 |
. . . . 5
⊢ (𝑡 = dom dom 𝐺 → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(dom dom 𝐺 × dom dom 𝐺)⟶dom dom 𝐺)) |
42 | | ismgmOLD.1 |
. . . . . . . 8
⊢ 𝑋 = dom dom 𝐺 |
43 | 42 | eqcomi 2631 |
. . . . . . 7
⊢ dom dom
𝐺 = 𝑋 |
44 | 43, 43 | xpeq12i 5137 |
. . . . . 6
⊢ (dom dom
𝐺 × dom dom 𝐺) = (𝑋 × 𝑋) |
45 | 44, 43 | feq23i 6039 |
. . . . 5
⊢ (𝐺:(dom dom 𝐺 × dom dom 𝐺)⟶dom dom 𝐺 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋) |
46 | 41, 45 | syl6bb 276 |
. . . 4
⊢ (𝑡 = dom dom 𝐺 → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
47 | 46 | ceqsexgv 3335 |
. . 3
⊢ (dom dom
𝐺 ∈ V →
(∃𝑡(𝑡 = dom dom 𝐺 ∧ 𝐺:(𝑡 × 𝑡)⟶𝑡) ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
48 | 36, 37, 47 | 3syl 18 |
. 2
⊢ (𝐺 ∈ 𝐴 → (∃𝑡(𝑡 = dom dom 𝐺 ∧ 𝐺:(𝑡 × 𝑡)⟶𝑡) ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
49 | 35, 48 | bitrd 268 |
1
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |