| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | basfn 17251 | . . 3
⊢ Base Fn
V | 
| 2 |  | ssv 4008 | . . 3
⊢ Grp
⊆ V | 
| 3 |  | fvelimab 6981 | . . 3
⊢ ((Base Fn
V ∧ Grp ⊆ V) → ((𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp) ↔
∃𝑥 ∈ Grp
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆)))) | 
| 4 | 1, 2, 3 | mp2an 692 | . 2
⊢ ((𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp)
↔ ∃𝑥 ∈ Grp
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) | 
| 5 |  | harcl 9599 | . . . . . 6
⊢
(har‘𝑆) ∈
On | 
| 6 |  | onenon 9989 | . . . . . 6
⊢
((har‘𝑆)
∈ On → (har‘𝑆) ∈ dom card) | 
| 7 | 5, 6 | ax-mp 5 | . . . . 5
⊢
(har‘𝑆) ∈
dom card | 
| 8 |  | xpnum 9991 | . . . . 5
⊢
(((har‘𝑆)
∈ dom card ∧ (har‘𝑆) ∈ dom card) → ((har‘𝑆) × (har‘𝑆)) ∈ dom
card) | 
| 9 | 7, 7, 8 | mp2an 692 | . . . 4
⊢
((har‘𝑆)
× (har‘𝑆))
∈ dom card | 
| 10 |  | ssun1 4178 | . . . . . . . 8
⊢ 𝑆 ⊆ (𝑆 ∪ (har‘𝑆)) | 
| 11 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → (Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) | 
| 12 | 10, 11 | sseqtrrid 4027 | . . . . . . 7
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → 𝑆 ⊆ (Base‘𝑥)) | 
| 13 |  | fvex 6919 | . . . . . . . 8
⊢
(Base‘𝑥)
∈ V | 
| 14 | 13 | ssex 5321 | . . . . . . 7
⊢ (𝑆 ⊆ (Base‘𝑥) → 𝑆 ∈ V) | 
| 15 | 12, 14 | syl 17 | . . . . . 6
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → 𝑆 ∈ V) | 
| 16 | 7 | a1i 11 | . . . . . 6
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → (har‘𝑆) ∈ dom
card) | 
| 17 |  | simp1l 1198 | . . . . . . . 8
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → 𝑥 ∈ Grp) | 
| 18 | 12 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → 𝑆 ⊆ (Base‘𝑥)) | 
| 19 |  | simp2 1138 | . . . . . . . . 9
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → 𝑎 ∈ 𝑆) | 
| 20 | 18, 19 | sseldd 3984 | . . . . . . . 8
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → 𝑎 ∈ (Base‘𝑥)) | 
| 21 |  | ssun2 4179 | . . . . . . . . . . 11
⊢
(har‘𝑆)
⊆ (𝑆 ∪
(har‘𝑆)) | 
| 22 | 21, 11 | sseqtrrid 4027 | . . . . . . . . . 10
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → (har‘𝑆) ⊆ (Base‘𝑥)) | 
| 23 | 22 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → (har‘𝑆) ⊆ (Base‘𝑥)) | 
| 24 |  | simp3 1139 | . . . . . . . . 9
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → 𝑐 ∈ (har‘𝑆)) | 
| 25 | 23, 24 | sseldd 3984 | . . . . . . . 8
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → 𝑐 ∈ (Base‘𝑥)) | 
| 26 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘𝑥) =
(Base‘𝑥) | 
| 27 |  | eqid 2737 | . . . . . . . . 9
⊢
(+g‘𝑥) = (+g‘𝑥) | 
| 28 | 26, 27 | grpcl 18959 | . . . . . . . 8
⊢ ((𝑥 ∈ Grp ∧ 𝑎 ∈ (Base‘𝑥) ∧ 𝑐 ∈ (Base‘𝑥)) → (𝑎(+g‘𝑥)𝑐) ∈ (Base‘𝑥)) | 
| 29 | 17, 20, 25, 28 | syl3anc 1373 | . . . . . . 7
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → (𝑎(+g‘𝑥)𝑐) ∈ (Base‘𝑥)) | 
| 30 |  | simp1r 1199 | . . . . . . 7
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → (Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) | 
| 31 | 29, 30 | eleqtrd 2843 | . . . . . 6
⊢ (((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ (har‘𝑆)) → (𝑎(+g‘𝑥)𝑐) ∈ (𝑆 ∪ (har‘𝑆))) | 
| 32 |  | simplll 775 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑥 ∈ Grp) | 
| 33 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → (har‘𝑆) ⊆ (Base‘𝑥)) | 
| 34 |  | simprl 771 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑐 ∈ (har‘𝑆)) | 
| 35 | 33, 34 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑐 ∈ (Base‘𝑥)) | 
| 36 |  | simprr 773 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑑 ∈ (har‘𝑆)) | 
| 37 | 33, 36 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑑 ∈ (Base‘𝑥)) | 
| 38 | 12 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑆 ⊆ (Base‘𝑥)) | 
| 39 |  | simplr 769 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑎 ∈ 𝑆) | 
| 40 | 38, 39 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → 𝑎 ∈ (Base‘𝑥)) | 
| 41 | 26, 27 | grplcan 19018 | . . . . . . 7
⊢ ((𝑥 ∈ Grp ∧ (𝑐 ∈ (Base‘𝑥) ∧ 𝑑 ∈ (Base‘𝑥) ∧ 𝑎 ∈ (Base‘𝑥))) → ((𝑎(+g‘𝑥)𝑐) = (𝑎(+g‘𝑥)𝑑) ↔ 𝑐 = 𝑑)) | 
| 42 | 32, 35, 37, 40, 41 | syl13anc 1374 | . . . . . 6
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑎 ∈ 𝑆) ∧ (𝑐 ∈ (har‘𝑆) ∧ 𝑑 ∈ (har‘𝑆))) → ((𝑎(+g‘𝑥)𝑐) = (𝑎(+g‘𝑥)𝑑) ↔ 𝑐 = 𝑑)) | 
| 43 |  | simplll 775 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑥 ∈ Grp) | 
| 44 | 12 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑆 ⊆ (Base‘𝑥)) | 
| 45 |  | simprr 773 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑑 ∈ 𝑆) | 
| 46 | 44, 45 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑑 ∈ (Base‘𝑥)) | 
| 47 |  | simprl 771 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑎 ∈ 𝑆) | 
| 48 | 44, 47 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑎 ∈ (Base‘𝑥)) | 
| 49 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → (har‘𝑆) ⊆ (Base‘𝑥)) | 
| 50 |  | simplr 769 | . . . . . . . 8
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑏 ∈ (har‘𝑆)) | 
| 51 | 49, 50 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → 𝑏 ∈ (Base‘𝑥)) | 
| 52 | 26, 27 | grprcan 18991 | . . . . . . 7
⊢ ((𝑥 ∈ Grp ∧ (𝑑 ∈ (Base‘𝑥) ∧ 𝑎 ∈ (Base‘𝑥) ∧ 𝑏 ∈ (Base‘𝑥))) → ((𝑑(+g‘𝑥)𝑏) = (𝑎(+g‘𝑥)𝑏) ↔ 𝑑 = 𝑎)) | 
| 53 | 43, 46, 48, 51, 52 | syl13anc 1374 | . . . . . 6
⊢ ((((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) ∧ 𝑏 ∈ (har‘𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → ((𝑑(+g‘𝑥)𝑏) = (𝑎(+g‘𝑥)𝑏) ↔ 𝑑 = 𝑎)) | 
| 54 |  | harndom 9602 | . . . . . . 7
⊢  ¬
(har‘𝑆) ≼ 𝑆 | 
| 55 | 54 | a1i 11 | . . . . . 6
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → ¬
(har‘𝑆) ≼ 𝑆) | 
| 56 | 15, 16, 16, 31, 42, 53, 55 | unxpwdom3 43107 | . . . . 5
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → 𝑆 ≼* ((har‘𝑆) × (har‘𝑆))) | 
| 57 |  | wdomnumr 10104 | . . . . . 6
⊢
(((har‘𝑆)
× (har‘𝑆))
∈ dom card → (𝑆
≼* ((har‘𝑆) × (har‘𝑆)) ↔ 𝑆 ≼ ((har‘𝑆) × (har‘𝑆)))) | 
| 58 | 9, 57 | ax-mp 5 | . . . . 5
⊢ (𝑆 ≼*
((har‘𝑆) ×
(har‘𝑆)) ↔ 𝑆 ≼ ((har‘𝑆) × (har‘𝑆))) | 
| 59 | 56, 58 | sylib 218 | . . . 4
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → 𝑆 ≼ ((har‘𝑆) × (har‘𝑆))) | 
| 60 |  | numdom 10078 | . . . 4
⊢
((((har‘𝑆)
× (har‘𝑆))
∈ dom card ∧ 𝑆
≼ ((har‘𝑆)
× (har‘𝑆)))
→ 𝑆 ∈ dom
card) | 
| 61 | 9, 59, 60 | sylancr 587 | . . 3
⊢ ((𝑥 ∈ Grp ∧
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆))) → 𝑆 ∈ dom card) | 
| 62 | 61 | rexlimiva 3147 | . 2
⊢
(∃𝑥 ∈ Grp
(Base‘𝑥) = (𝑆 ∪ (har‘𝑆)) → 𝑆 ∈ dom card) | 
| 63 | 4, 62 | sylbi 217 | 1
⊢ ((𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp)
→ 𝑆 ∈ dom
card) |