| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tocyccntz.s | . 2
⊢ 𝑆 = (SymGrp‘𝐷) | 
| 2 |  | eqid 2736 | . 2
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 3 |  | tocyccntz.z | . 2
⊢ 𝑍 = (Cntz‘𝑆) | 
| 4 |  | tocyccntz.1 | . . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) | 
| 5 |  | tocyccntz.m | . . . 4
⊢ 𝑀 = (toCyc‘𝐷) | 
| 6 | 5, 1, 2 | tocycf 33138 | . . 3
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}⟶(Base‘𝑆)) | 
| 7 |  | fimass 6755 | . . 3
⊢ (𝑀:{𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}⟶(Base‘𝑆) → (𝑀 “ 𝐴) ⊆ (Base‘𝑆)) | 
| 8 | 4, 6, 7 | 3syl 18 | . 2
⊢ (𝜑 → (𝑀 “ 𝐴) ⊆ (Base‘𝑆)) | 
| 9 |  | difss 4135 | . . . . . . 7
⊢ (𝐴 ∖ (◡♯ “ {0, 1})) ⊆ 𝐴 | 
| 10 |  | tocyccntz.2 | . . . . . . 7
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ran 𝑥) | 
| 11 |  | disjss1 5115 | . . . . . . 7
⊢ ((𝐴 ∖ (◡♯ “ {0, 1})) ⊆ 𝐴 → (Disj 𝑥 ∈ 𝐴 ran 𝑥 → Disj 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))ran 𝑥)) | 
| 12 | 9, 10, 11 | mpsyl 68 | . . . . . 6
⊢ (𝜑 → Disj 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))ran 𝑥) | 
| 13 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝐷 ∈ 𝑉) | 
| 14 |  | tocyccntz.a | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ dom 𝑀) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝐴 ⊆ dom 𝑀) | 
| 16 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) | 
| 17 | 16 | eldifad 3962 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑥 ∈ 𝐴) | 
| 18 | 15, 17 | sseldd 3983 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑥 ∈ dom 𝑀) | 
| 19 |  | fdm 6744 | . . . . . . . . . . . . 13
⊢ (𝑀:{𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}⟶(Base‘𝑆) → dom 𝑀 = {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 20 | 13, 6, 19 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → dom 𝑀 = {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 21 | 18, 20 | eleqtrd 2842 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑥 ∈ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 22 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑥 → 𝑐 = 𝑥) | 
| 23 |  | dmeq 5913 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑥 → dom 𝑐 = dom 𝑥) | 
| 24 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑥 → 𝐷 = 𝐷) | 
| 25 | 22, 23, 24 | f1eq123d 6839 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑥 → (𝑐:dom 𝑐–1-1→𝐷 ↔ 𝑥:dom 𝑥–1-1→𝐷)) | 
| 26 | 25 | elrab 3691 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷} ↔ (𝑥 ∈ Word 𝐷 ∧ 𝑥:dom 𝑥–1-1→𝐷)) | 
| 27 | 21, 26 | sylib 218 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → (𝑥 ∈ Word 𝐷 ∧ 𝑥:dom 𝑥–1-1→𝐷)) | 
| 28 | 27 | simpld 494 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑥 ∈ Word 𝐷) | 
| 29 | 27 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑥:dom 𝑥–1-1→𝐷) | 
| 30 | 16 | eldifbd 3963 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → ¬ 𝑥 ∈ (◡♯ “ {0, 1})) | 
| 31 |  | hashgt1 32813 | . . . . . . . . . . 11
⊢ (𝑥 ∈ V → (¬ 𝑥 ∈ (◡♯ “ {0, 1}) ↔ 1 <
(♯‘𝑥))) | 
| 32 | 31 | elv 3484 | . . . . . . . . . 10
⊢ (¬
𝑥 ∈ (◡♯ “ {0, 1}) ↔ 1 <
(♯‘𝑥)) | 
| 33 | 30, 32 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 1 <
(♯‘𝑥)) | 
| 34 | 5, 13, 28, 29, 33 | cycpmrn 33164 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → ran 𝑥 = dom ((𝑀‘𝑥) ∖ I )) | 
| 35 | 16 | fvresd 6925 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) = (𝑀‘𝑥)) | 
| 36 | 35 | difeq1d 4124 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I ) = ((𝑀‘𝑥) ∖ I )) | 
| 37 | 36 | dmeqd 5915 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → dom
(((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I ) = dom ((𝑀‘𝑥) ∖ I )) | 
| 38 | 34, 37 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → ran 𝑥 = dom (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I )) | 
| 39 | 38 | disjeq2dv 5114 | . . . . . 6
⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))ran 𝑥 ↔ Disj 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))dom (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I ))) | 
| 40 | 12, 39 | mpbid 232 | . . . . 5
⊢ (𝜑 → Disj 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))dom (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I )) | 
| 41 | 4, 6 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀:{𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}⟶(Base‘𝑆)) | 
| 42 | 41 | ffdmd 6765 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀:dom 𝑀⟶(Base‘𝑆)) | 
| 43 | 14 | ssdifssd 4146 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∖ (◡♯ “ {0, 1})) ⊆ dom 𝑀) | 
| 44 | 42, 43 | fssresd 6774 | . . . . . . . . 9
⊢ (𝜑 → (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0,
1}))⟶(Base‘𝑆)) | 
| 45 | 41, 14 | fssdmd 6753 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ⊆ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 46 | 45 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝐴 ⊆ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 47 |  | simp-4r 783 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) | 
| 48 | 47 | eldifad 3962 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 ∈ 𝐴) | 
| 49 | 46, 48 | sseldd 3983 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 ∈ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 50 |  | id 22 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 𝑠 → 𝑐 = 𝑠) | 
| 51 |  | dmeq 5913 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 𝑠 → dom 𝑐 = dom 𝑠) | 
| 52 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 𝑠 → 𝐷 = 𝐷) | 
| 53 | 50, 51, 52 | f1eq123d 6839 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑠 → (𝑐:dom 𝑐–1-1→𝐷 ↔ 𝑠:dom 𝑠–1-1→𝐷)) | 
| 54 | 53 | elrab 3691 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷} ↔ (𝑠 ∈ Word 𝐷 ∧ 𝑠:dom 𝑠–1-1→𝐷)) | 
| 55 | 49, 54 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → (𝑠 ∈ Word 𝐷 ∧ 𝑠:dom 𝑠–1-1→𝐷)) | 
| 56 | 55 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 ∈ Word 𝐷) | 
| 57 |  | wrdf 14558 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ Word 𝐷 → 𝑠:(0..^(♯‘𝑠))⟶𝐷) | 
| 58 |  | frel 6740 | . . . . . . . . . . . . . . . 16
⊢ (𝑠:(0..^(♯‘𝑠))⟶𝐷 → Rel 𝑠) | 
| 59 | 56, 57, 58 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → Rel 𝑠) | 
| 60 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) | 
| 61 | 47 | fvresd 6925 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = (𝑀‘𝑠)) | 
| 62 | 16 | ad5ant13 756 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) | 
| 63 | 62 | fvresd 6925 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) = (𝑀‘𝑥)) | 
| 64 | 60, 61, 63 | 3eqtr3rd 2785 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → (𝑀‘𝑥) = (𝑀‘𝑠)) | 
| 65 | 64 | difeq1d 4124 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ((𝑀‘𝑥) ∖ I ) = ((𝑀‘𝑠) ∖ I )) | 
| 66 | 65 | dmeqd 5915 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → dom ((𝑀‘𝑥) ∖ I ) = dom ((𝑀‘𝑠) ∖ I )) | 
| 67 | 4 | ad4antr 732 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝐷 ∈ 𝑉) | 
| 68 | 17 | ad5ant13 756 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥 ∈ 𝐴) | 
| 69 | 46, 68 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥 ∈ {𝑐 ∈ Word 𝐷 ∣ 𝑐:dom 𝑐–1-1→𝐷}) | 
| 70 | 69, 26 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → (𝑥 ∈ Word 𝐷 ∧ 𝑥:dom 𝑥–1-1→𝐷)) | 
| 71 | 70 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥 ∈ Word 𝐷) | 
| 72 | 70 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥:dom 𝑥–1-1→𝐷) | 
| 73 | 33 | ad5ant13 756 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 1 < (♯‘𝑥)) | 
| 74 | 5, 67, 71, 72, 73 | cycpmrn 33164 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ran 𝑥 = dom ((𝑀‘𝑥) ∖ I )) | 
| 75 | 55 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠:dom 𝑠–1-1→𝐷) | 
| 76 | 14 | ssdifd 4144 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 ∖ (◡♯ “ {0, 1})) ⊆ (dom 𝑀 ∖ (◡♯ “ {0, 1}))) | 
| 77 | 76 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → 𝑠 ∈ (dom 𝑀 ∖ (◡♯ “ {0, 1}))) | 
| 78 | 77 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 ∈ (dom 𝑀 ∖ (◡♯ “ {0, 1}))) | 
| 79 | 78 | eldifbd 3963 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ¬ 𝑠 ∈ (◡♯ “ {0, 1})) | 
| 80 |  | hashgt1 32813 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ 𝐴 → (¬ 𝑠 ∈ (◡♯ “ {0, 1}) ↔ 1 <
(♯‘𝑠))) | 
| 81 | 80 | biimpa 476 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ∈ (◡♯ “ {0, 1})) → 1 <
(♯‘𝑠)) | 
| 82 | 48, 79, 81 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 1 < (♯‘𝑠)) | 
| 83 | 5, 67, 56, 75, 82 | cycpmrn 33164 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ran 𝑠 = dom ((𝑀‘𝑠) ∖ I )) | 
| 84 | 66, 74, 83 | 3eqtr4rd 2787 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ran 𝑠 = ran 𝑥) | 
| 85 | 84 | ineq2d 4219 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → (ran 𝑥 ∩ ran 𝑠) = (ran 𝑥 ∩ ran 𝑥)) | 
| 86 |  | inidm 4226 | . . . . . . . . . . . . . . . . . 18
⊢ (ran
𝑥 ∩ ran 𝑥) = ran 𝑥 | 
| 87 | 85, 86 | eqtrdi 2792 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → (ran 𝑥 ∩ ran 𝑠) = ran 𝑥) | 
| 88 |  | rneq 5946 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ran 𝑥 = ran 𝑦) | 
| 89 | 88 | cbvdisjv 5120 | . . . . . . . . . . . . . . . . . . . 20
⊢
(Disj 𝑥
∈ 𝐴 ran 𝑥 ↔ Disj 𝑦 ∈ 𝐴 ran 𝑦) | 
| 90 | 10, 89 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ran 𝑦) | 
| 91 | 90 | ad4antr 732 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → Disj 𝑦 ∈ 𝐴 ran 𝑦) | 
| 92 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ¬ 𝑠 = 𝑥) | 
| 93 | 92 | neqned 2946 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 ≠ 𝑥) | 
| 94 | 93 | necomd 2995 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥 ≠ 𝑠) | 
| 95 |  | rneq 5946 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ran 𝑦 = ran 𝑥) | 
| 96 |  | rneq 5946 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑠 → ran 𝑦 = ran 𝑠) | 
| 97 | 95, 96 | disji2 5126 | . . . . . . . . . . . . . . . . . 18
⊢
((Disj 𝑦
∈ 𝐴 ran 𝑦 ∧ (𝑥 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ≠ 𝑠) → (ran 𝑥 ∩ ran 𝑠) = ∅) | 
| 98 | 91, 68, 48, 94, 97 | syl121anc 1376 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → (ran 𝑥 ∩ ran 𝑠) = ∅) | 
| 99 | 87, 98 | eqtr3d 2778 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ran 𝑥 = ∅) | 
| 100 | 84, 99 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → ran 𝑠 = ∅) | 
| 101 |  | relrn0 5982 | . . . . . . . . . . . . . . . 16
⊢ (Rel
𝑠 → (𝑠 = ∅ ↔ ran 𝑠 = ∅)) | 
| 102 | 101 | biimpar 477 | . . . . . . . . . . . . . . 15
⊢ ((Rel
𝑠 ∧ ran 𝑠 = ∅) → 𝑠 = ∅) | 
| 103 | 59, 100, 102 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 = ∅) | 
| 104 |  | wrdf 14558 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word 𝐷 → 𝑥:(0..^(♯‘𝑥))⟶𝐷) | 
| 105 |  | frel 6740 | . . . . . . . . . . . . . . . 16
⊢ (𝑥:(0..^(♯‘𝑥))⟶𝐷 → Rel 𝑥) | 
| 106 | 71, 104, 105 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → Rel 𝑥) | 
| 107 |  | relrn0 5982 | . . . . . . . . . . . . . . . 16
⊢ (Rel
𝑥 → (𝑥 = ∅ ↔ ran 𝑥 = ∅)) | 
| 108 | 107 | biimpar 477 | . . . . . . . . . . . . . . 15
⊢ ((Rel
𝑥 ∧ ran 𝑥 = ∅) → 𝑥 = ∅) | 
| 109 | 106, 99, 108 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑥 = ∅) | 
| 110 | 103, 109 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) ∧ ¬ 𝑠 = 𝑥) → 𝑠 = 𝑥) | 
| 111 | 110 | pm2.18da 799 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) → 𝑠 = 𝑥) | 
| 112 | 111 | ex 412 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))) → (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) → 𝑠 = 𝑥)) | 
| 113 | 112 | anasss 466 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1})) ∧ 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1})))) → (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) → 𝑠 = 𝑥)) | 
| 114 | 113 | ralrimivva 3201 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑠 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))∀𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))(((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) → 𝑠 = 𝑥)) | 
| 115 |  | dff13 7276 | . . . . . . . . 9
⊢ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1→(Base‘𝑆) ↔ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0,
1}))⟶(Base‘𝑆)
∧ ∀𝑠 ∈
(𝐴 ∖ (◡♯ “ {0, 1}))∀𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))(((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑠) = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) → 𝑠 = 𝑥))) | 
| 116 | 44, 114, 115 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 → (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1→(Base‘𝑆)) | 
| 117 |  | f1f1orn 6858 | . . . . . . . 8
⊢ ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1→(Base‘𝑆) → (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1-onto→ran
(𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))) | 
| 118 | 116, 117 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1-onto→ran
(𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))) | 
| 119 |  | df-ima 5697 | . . . . . . . . 9
⊢ (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) = ran (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))) | 
| 120 | 119 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) = ran (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))) | 
| 121 | 120 | f1oeq3d 6844 | . . . . . . 7
⊢ (𝜑 → ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1-onto→(𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ↔ (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1-onto→ran
(𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))))) | 
| 122 | 118, 121 | mpbird 257 | . . . . . 6
⊢ (𝜑 → (𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1}))):(𝐴 ∖ (◡♯ “ {0, 1}))–1-1-onto→(𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1})))) | 
| 123 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) → 𝑐 = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) | 
| 124 | 123 | difeq1d 4124 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) → (𝑐 ∖ I ) = (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I )) | 
| 125 | 124 | dmeqd 5915 | . . . . . 6
⊢ ((𝜑 ∧ 𝑐 = ((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥)) → dom (𝑐 ∖ I ) = dom (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I )) | 
| 126 | 122, 125 | disjrdx 32605 | . . . . 5
⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∖ (◡♯ “ {0, 1}))dom (((𝑀 ↾ (𝐴 ∖ (◡♯ “ {0, 1})))‘𝑥) ∖ I ) ↔ Disj
𝑐 ∈ (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1})))dom (𝑐 ∖ I ))) | 
| 127 | 40, 126 | mpbid 232 | . . . 4
⊢ (𝜑 → Disj 𝑐 ∈ (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1})))dom (𝑐 ∖ I )) | 
| 128 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → (𝑀‘𝑥) = 𝑐) | 
| 129 | 4 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → 𝐷 ∈ 𝑉) | 
| 130 | 14 | ssrind 4243 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∩ (◡♯ “ {0, 1})) ⊆ (dom 𝑀 ∩ (◡♯ “ {0, 1}))) | 
| 131 | 130 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → (𝐴 ∩ (◡♯ “ {0, 1})) ⊆ (dom 𝑀 ∩ (◡♯ “ {0, 1}))) | 
| 132 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) | 
| 133 | 131, 132 | sseldd 3983 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → 𝑥 ∈ (dom 𝑀 ∩ (◡♯ “ {0, 1}))) | 
| 134 | 5 | tocyc01 33139 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑥 ∈ (dom 𝑀 ∩ (◡♯ “ {0, 1}))) → (𝑀‘𝑥) = ( I ↾ 𝐷)) | 
| 135 | 129, 133,
134 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → (𝑀‘𝑥) = ( I ↾ 𝐷)) | 
| 136 | 128, 135 | eqtr3d 2778 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → 𝑐 = ( I ↾ 𝐷)) | 
| 137 | 136 | difeq1d 4124 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → (𝑐 ∖ I ) = (( I ↾ 𝐷) ∖ I )) | 
| 138 | 137 | dmeqd 5915 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → dom (𝑐 ∖ I ) = dom (( I ↾ 𝐷) ∖ I )) | 
| 139 |  | resdifcom 6015 | . . . . . . . . . 10
⊢ (( I
↾ 𝐷) ∖ I ) = ((
I ∖ I ) ↾ 𝐷) | 
| 140 |  | difid 4375 | . . . . . . . . . . 11
⊢ ( I
∖ I ) = ∅ | 
| 141 | 140 | reseq1i 5992 | . . . . . . . . . 10
⊢ (( I
∖ I ) ↾ 𝐷) =
(∅ ↾ 𝐷) | 
| 142 |  | 0res 32617 | . . . . . . . . . 10
⊢ (∅
↾ 𝐷) =
∅ | 
| 143 | 139, 141,
142 | 3eqtri 2768 | . . . . . . . . 9
⊢ (( I
↾ 𝐷) ∖ I ) =
∅ | 
| 144 | 143 | dmeqi 5914 | . . . . . . . 8
⊢ dom (( I
↾ 𝐷) ∖ I ) =
dom ∅ | 
| 145 |  | dm0 5930 | . . . . . . . 8
⊢ dom
∅ = ∅ | 
| 146 | 144, 145 | eqtri 2764 | . . . . . . 7
⊢ dom (( I
↾ 𝐷) ∖ I ) =
∅ | 
| 147 | 138, 146 | eqtrdi 2792 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) ∧ 𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))) ∧ (𝑀‘𝑥) = 𝑐) → dom (𝑐 ∖ I ) = ∅) | 
| 148 | 41 | ffund 6739 | . . . . . . 7
⊢ (𝜑 → Fun 𝑀) | 
| 149 |  | fvelima 6973 | . . . . . . 7
⊢ ((Fun
𝑀 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) →
∃𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))(𝑀‘𝑥) = 𝑐) | 
| 150 | 148, 149 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) →
∃𝑥 ∈ (𝐴 ∩ (◡♯ “ {0, 1}))(𝑀‘𝑥) = 𝑐) | 
| 151 | 147, 150 | r19.29a 3161 | . . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) → dom (𝑐 ∖ I ) =
∅) | 
| 152 | 151 | disjxun0 32588 | . . . 4
⊢ (𝜑 → (Disj 𝑐 ∈ ((𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1}))))dom (𝑐 ∖ I ) ↔ Disj
𝑐 ∈ (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1})))dom (𝑐 ∖ I ))) | 
| 153 | 127, 152 | mpbird 257 | . . 3
⊢ (𝜑 → Disj 𝑐 ∈ ((𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1}))))dom (𝑐 ∖ I )) | 
| 154 |  | uncom 4157 | . . . . . 6
⊢ ((𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) = ((𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1})))) | 
| 155 |  | imaundi 6168 | . . . . . 6
⊢ (𝑀 “ ((𝐴 ∩ (◡♯ “ {0, 1})) ∪ (𝐴 ∖ (◡♯ “ {0, 1})))) = ((𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1})))) | 
| 156 |  | inundif 4478 | . . . . . . 7
⊢ ((𝐴 ∩ (◡♯ “ {0, 1})) ∪ (𝐴 ∖ (◡♯ “ {0, 1}))) = 𝐴 | 
| 157 | 156 | imaeq2i 6075 | . . . . . 6
⊢ (𝑀 “ ((𝐴 ∩ (◡♯ “ {0, 1})) ∪ (𝐴 ∖ (◡♯ “ {0, 1})))) = (𝑀 “ 𝐴) | 
| 158 | 154, 155,
157 | 3eqtr2i 2770 | . . . . 5
⊢ ((𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) = (𝑀 “ 𝐴) | 
| 159 | 158 | a1i 11 | . . . 4
⊢ (𝜑 → ((𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1})))) = (𝑀 “ 𝐴)) | 
| 160 | 159 | disjeq1d 5117 | . . 3
⊢ (𝜑 → (Disj 𝑐 ∈ ((𝑀 “ (𝐴 ∖ (◡♯ “ {0, 1}))) ∪ (𝑀 “ (𝐴 ∩ (◡♯ “ {0, 1}))))dom (𝑐 ∖ I ) ↔ Disj
𝑐 ∈ (𝑀 “ 𝐴)dom (𝑐 ∖ I ))) | 
| 161 | 153, 160 | mpbid 232 | . 2
⊢ (𝜑 → Disj 𝑐 ∈ (𝑀 “ 𝐴)dom (𝑐 ∖ I )) | 
| 162 | 1, 2, 3, 8, 161 | symgcntz 33106 | 1
⊢ (𝜑 → (𝑀 “ 𝐴) ⊆ (𝑍‘(𝑀 “ 𝐴))) |