Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝐺)
∈ V |
2 | 1 | rabex 4740 |
. . . . . . . 8
⊢ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ V |
3 | | simp2l 1080 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑦 ∈ (SubGrp‘𝐺)) |
4 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺) =
(Base‘𝐺) |
5 | 4 | subgss 17418 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (SubGrp‘𝐺) → 𝑦 ⊆ (Base‘𝐺)) |
6 | 3, 5 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑦 ⊆ (Base‘𝐺)) |
7 | | simpl2l 1107 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑦) → 𝑦 ∈ (SubGrp‘𝐺)) |
8 | | simp3l 1082 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘𝑦) = 𝑁) |
9 | | simp1r 1079 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑁 ∈ ℕ) |
10 | 9 | nnnn0d 11228 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑁 ∈
ℕ0) |
11 | 8, 10 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘𝑦) ∈
ℕ0) |
12 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
13 | | hashclb 13011 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ V → (𝑦 ∈ Fin ↔
(#‘𝑦) ∈
ℕ0)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin ↔
(#‘𝑦) ∈
ℕ0) |
15 | 11, 14 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑦 ∈ Fin) |
16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑦) → 𝑦 ∈ Fin) |
17 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑦) |
18 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(od‘𝐺) =
(od‘𝐺) |
19 | 18 | odsubdvds 17809 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ 𝑦) → ((od‘𝐺)‘𝑧) ∥ (#‘𝑦)) |
20 | 7, 16, 17, 19 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑦) → ((od‘𝐺)‘𝑧) ∥ (#‘𝑦)) |
21 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑦) → (#‘𝑦) = 𝑁) |
22 | 20, 21 | breqtrd 4609 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑦) → ((od‘𝐺)‘𝑧) ∥ 𝑁) |
23 | 6, 22 | ssrabdv 3644 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑦 ⊆ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) |
24 | | simp2r 1081 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑥 ∈ (SubGrp‘𝐺)) |
25 | 4 | subgss 17418 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ (Base‘𝐺)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑥 ⊆ (Base‘𝐺)) |
27 | | simpl2r 1108 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ (SubGrp‘𝐺)) |
28 | | simp3r 1083 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘𝑥) = 𝑁) |
29 | 28, 10 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘𝑥) ∈
ℕ0) |
30 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
31 | | hashclb 13011 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → (𝑥 ∈ Fin ↔
(#‘𝑥) ∈
ℕ0)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ Fin ↔
(#‘𝑥) ∈
ℕ0) |
33 | 29, 32 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑥 ∈ Fin) |
34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ Fin) |
35 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑥) |
36 | 18 | odsubdvds 17809 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ Fin ∧ 𝑧 ∈ 𝑥) → ((od‘𝐺)‘𝑧) ∥ (#‘𝑥)) |
37 | 27, 34, 35, 36 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑥) → ((od‘𝐺)‘𝑧) ∥ (#‘𝑥)) |
38 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑥) → (#‘𝑥) = 𝑁) |
39 | 37, 38 | breqtrd 4609 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) ∧ 𝑧 ∈ 𝑥) → ((od‘𝐺)‘𝑧) ∥ 𝑁) |
40 | 26, 39 | ssrabdv 3644 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑥 ⊆ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) |
41 | 23, 40 | unssd 3751 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (𝑦 ∪ 𝑥) ⊆ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) |
42 | | ssdomg 7887 |
. . . . . . . 8
⊢ ({𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ V → ((𝑦 ∪ 𝑥) ⊆ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} → (𝑦 ∪ 𝑥) ≼ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁})) |
43 | 2, 41, 42 | mpsyl 66 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (𝑦 ∪ 𝑥) ≼ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) |
44 | | idomsubgmo.g |
. . . . . . . . . . 11
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s
(Unit‘𝑅)) |
45 | 44, 4, 18 | idomodle 36793 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑧 ∈
(Base‘𝐺) ∣
((od‘𝐺)‘𝑧) ∥ 𝑁}) ≤ 𝑁) |
46 | 45 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘{𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) ≤ 𝑁) |
47 | 46, 8 | breqtrrd 4611 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘{𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) ≤ (#‘𝑦)) |
48 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ V) |
49 | | hashbnd 12985 |
. . . . . . . . . 10
⊢ (({𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ V ∧ (#‘𝑦) ∈ ℕ0 ∧
(#‘{𝑧 ∈
(Base‘𝐺) ∣
((od‘𝐺)‘𝑧) ∥ 𝑁}) ≤ (#‘𝑦)) → {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ Fin) |
50 | 48, 11, 47, 49 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ Fin) |
51 | | hashdom 13029 |
. . . . . . . . 9
⊢ (({𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∈ Fin ∧ 𝑦 ∈ V) → ((#‘{𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) ≤ (#‘𝑦) ↔ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ≼ 𝑦)) |
52 | 50, 12, 51 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → ((#‘{𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁}) ≤ (#‘𝑦) ↔ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ≼ 𝑦)) |
53 | 47, 52 | mpbid 221 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ≼ 𝑦) |
54 | | domtr 7895 |
. . . . . . 7
⊢ (((𝑦 ∪ 𝑥) ≼ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ∧ {𝑧 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑧) ∥ 𝑁} ≼ 𝑦) → (𝑦 ∪ 𝑥) ≼ 𝑦) |
55 | 43, 53, 54 | syl2anc 691 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (𝑦 ∪ 𝑥) ≼ 𝑦) |
56 | 12, 30 | unex 6854 |
. . . . . . 7
⊢ (𝑦 ∪ 𝑥) ∈ V |
57 | | ssun1 3738 |
. . . . . . 7
⊢ 𝑦 ⊆ (𝑦 ∪ 𝑥) |
58 | | ssdomg 7887 |
. . . . . . 7
⊢ ((𝑦 ∪ 𝑥) ∈ V → (𝑦 ⊆ (𝑦 ∪ 𝑥) → 𝑦 ≼ (𝑦 ∪ 𝑥))) |
59 | 56, 57, 58 | mp2 9 |
. . . . . 6
⊢ 𝑦 ≼ (𝑦 ∪ 𝑥) |
60 | | sbth 7965 |
. . . . . 6
⊢ (((𝑦 ∪ 𝑥) ≼ 𝑦 ∧ 𝑦 ≼ (𝑦 ∪ 𝑥)) → (𝑦 ∪ 𝑥) ≈ 𝑦) |
61 | 55, 59, 60 | sylancl 693 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (𝑦 ∪ 𝑥) ≈ 𝑦) |
62 | 8, 28 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → (#‘𝑦) = (#‘𝑥)) |
63 | | hashen 12997 |
. . . . . . . 8
⊢ ((𝑦 ∈ Fin ∧ 𝑥 ∈ Fin) →
((#‘𝑦) =
(#‘𝑥) ↔ 𝑦 ≈ 𝑥)) |
64 | 15, 33, 63 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → ((#‘𝑦) = (#‘𝑥) ↔ 𝑦 ≈ 𝑥)) |
65 | 62, 64 | mpbid 221 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑦 ≈ 𝑥) |
66 | | fiuneneq 36794 |
. . . . . 6
⊢ ((𝑦 ≈ 𝑥 ∧ 𝑦 ∈ Fin) → ((𝑦 ∪ 𝑥) ≈ 𝑦 ↔ 𝑦 = 𝑥)) |
67 | 65, 15, 66 | syl2anc 691 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → ((𝑦 ∪ 𝑥) ≈ 𝑦 ↔ 𝑦 = 𝑥)) |
68 | 61, 67 | mpbid 221 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺)) ∧ ((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁)) → 𝑦 = 𝑥) |
69 | 68 | 3expia 1259 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (SubGrp‘𝐺))) → (((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁) → 𝑦 = 𝑥)) |
70 | 69 | ralrimivva 2954 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
∀𝑦 ∈
(SubGrp‘𝐺)∀𝑥 ∈ (SubGrp‘𝐺)(((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁) → 𝑦 = 𝑥)) |
71 | | fveq2 6103 |
. . . 4
⊢ (𝑦 = 𝑥 → (#‘𝑦) = (#‘𝑥)) |
72 | 71 | eqeq1d 2612 |
. . 3
⊢ (𝑦 = 𝑥 → ((#‘𝑦) = 𝑁 ↔ (#‘𝑥) = 𝑁)) |
73 | 72 | rmo4 3366 |
. 2
⊢
(∃*𝑦 ∈
(SubGrp‘𝐺)(#‘𝑦) = 𝑁 ↔ ∀𝑦 ∈ (SubGrp‘𝐺)∀𝑥 ∈ (SubGrp‘𝐺)(((#‘𝑦) = 𝑁 ∧ (#‘𝑥) = 𝑁) → 𝑦 = 𝑥)) |
74 | 70, 73 | sylibr 223 |
1
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
∃*𝑦 ∈
(SubGrp‘𝐺)(#‘𝑦) = 𝑁) |