Metamath Proof Explorer

Theorem tocyccntz

Description: All elements of a (finite) set of cycles commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Hypotheses tocyccntz.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
tocyccntz.z ⊢ 𝑍 = ( Cntz ‘ 𝑆 )
tocyccntz.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
tocyccntz.1 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocyccntz.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ran 𝑥 )
tocyccntz.a ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝑀 )
Assertion tocyccntz ( 𝜑 → ( 𝑀 “ 𝐴 ) ⊆ ( 𝑍 ‘ ( 𝑀 “ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 tocyccntz.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 tocyccntz.z ⊢ 𝑍 = ( Cntz ‘ 𝑆 )
3 tocyccntz.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
4 tocyccntz.1 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5 tocyccntz.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ran 𝑥 )
6 tocyccntz.a ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝑀 )
7 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 3 1 7 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
9 fimass ⊢ ( 𝑀 : { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) → ( 𝑀 “ 𝐴 ) ⊆ ( Base ‘ 𝑆 ) )
10 4 8 9 3syl ⊢ ( 𝜑 → ( 𝑀 “ 𝐴 ) ⊆ ( Base ‘ 𝑆 ) )
11 difss ⊢ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ⊆ 𝐴
12 disjss1 ⊢ ( ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 ran 𝑥 → Disj 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ran 𝑥 ) )
13 11 5 12 mpsyl ⊢ ( 𝜑 → Disj 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ran 𝑥 )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝐷 ∈ 𝑉 )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝐴 ⊆ dom 𝑀 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
17 16 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑥 ∈ 𝐴 )
18 15 17 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑥 ∈ dom 𝑀 )
19 fdm ⊢ ( 𝑀 : { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) → dom 𝑀 = { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
20 14 8 19 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → dom 𝑀 = { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
21 18 20 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑥 ∈ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
22 id ⊢ ( 𝑐 = 𝑥 → 𝑐 = 𝑥 )
23 dmeq ⊢ ( 𝑐 = 𝑥 → dom 𝑐 = dom 𝑥 )
24 eqidd ⊢ ( 𝑐 = 𝑥 → 𝐷 = 𝐷 )
25 22 23 24 f1eq123d ⊢ ( 𝑐 = 𝑥 → ( 𝑐 : dom 𝑐 –1-1→ 𝐷 ↔ 𝑥 : dom 𝑥 –1-1→ 𝐷 ) )
26 25 elrab ⊢ ( 𝑥 ∈ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } ↔ ( 𝑥 ∈ Word 𝐷 ∧ 𝑥 : dom 𝑥 –1-1→ 𝐷 ) )
27 21 26 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝑥 ∈ Word 𝐷 ∧ 𝑥 : dom 𝑥 –1-1→ 𝐷 ) )
28 27 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑥 ∈ Word 𝐷 )
29 27 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑥 : dom 𝑥 –1-1→ 𝐷 )
30 16 eldifbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ¬ 𝑥 ∈ ( ◡ ♯ “ { 0 , 1 } ) )
31 hashgt1 ⊢ ( 𝑥 ∈ V → ( ¬ 𝑥 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ 1 < ( ♯ ‘ 𝑥 ) ) )
32 31 elv ⊢ ( ¬ 𝑥 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ 1 < ( ♯ ‘ 𝑥 ) )
33 30 32 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 1 < ( ♯ ‘ 𝑥 ) )
34 3 14 28 29 33 cycpmrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ran 𝑥 = dom ( ( 𝑀 ‘ 𝑥 ) ∖ I ) )
35 16 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
36 35 difeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) = ( ( 𝑀 ‘ 𝑥 ) ∖ I ) )
37 36 dmeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → dom ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) = dom ( ( 𝑀 ‘ 𝑥 ) ∖ I ) )
38 34 37 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ran 𝑥 = dom ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) )
39 38 disjeq2dv ⊢ ( 𝜑 → ( Disj 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ran 𝑥 ↔ Disj 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) dom ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) ) )
40 13 39 mpbid ⊢ ( 𝜑 → Disj 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) dom ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) )
41 4 8 syl ⊢ ( 𝜑 → 𝑀 : { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
42 41 ffdmd ⊢ ( 𝜑 → 𝑀 : dom 𝑀 ⟶ ( Base ‘ 𝑆 ) )
43 6 ssdifssd ⊢ ( 𝜑 → ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ⊆ dom 𝑀 )
44 42 43 fssresd ⊢ ( 𝜑 → ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ⟶ ( Base ‘ 𝑆 ) )
45 41 6 fssdmd ⊢ ( 𝜑 → 𝐴 ⊆ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
46 45 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝐴 ⊆ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
47 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
48 47 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 ∈ 𝐴 )
49 46 48 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 ∈ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
50 id ⊢ ( 𝑐 = 𝑠 → 𝑐 = 𝑠 )
51 dmeq ⊢ ( 𝑐 = 𝑠 → dom 𝑐 = dom 𝑠 )
52 eqidd ⊢ ( 𝑐 = 𝑠 → 𝐷 = 𝐷 )
53 50 51 52 f1eq123d ⊢ ( 𝑐 = 𝑠 → ( 𝑐 : dom 𝑐 –1-1→ 𝐷 ↔ 𝑠 : dom 𝑠 –1-1→ 𝐷 ) )
54 53 elrab ⊢ ( 𝑠 ∈ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } ↔ ( 𝑠 ∈ Word 𝐷 ∧ 𝑠 : dom 𝑠 –1-1→ 𝐷 ) )
55 49 54 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( 𝑠 ∈ Word 𝐷 ∧ 𝑠 : dom 𝑠 –1-1→ 𝐷 ) )
56 55 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 ∈ Word 𝐷 )
57 wrdf ⊢ ( 𝑠 ∈ Word 𝐷 → 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐷 )
58 frel ⊢ ( 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐷 → Rel 𝑠 )
59 56 57 58 3syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → Rel 𝑠 )
60 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) )
61 47 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( 𝑀 ‘ 𝑠 ) )
62 16 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
63 62 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
64 60 61 63 3eqtr3rd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑠 ) )
65 64 difeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ( 𝑀 ‘ 𝑥 ) ∖ I ) = ( ( 𝑀 ‘ 𝑠 ) ∖ I ) )
66 65 dmeqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → dom ( ( 𝑀 ‘ 𝑥 ) ∖ I ) = dom ( ( 𝑀 ‘ 𝑠 ) ∖ I ) )
67 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝐷 ∈ 𝑉 )
68 17 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 ∈ 𝐴 )
69 46 68 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 ∈ { 𝑐 ∈ Word 𝐷 ∣ 𝑐 : dom 𝑐 –1-1→ 𝐷 } )
70 69 26 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( 𝑥 ∈ Word 𝐷 ∧ 𝑥 : dom 𝑥 –1-1→ 𝐷 ) )
71 70 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 ∈ Word 𝐷 )
72 70 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 : dom 𝑥 –1-1→ 𝐷 )
73 33 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 1 < ( ♯ ‘ 𝑥 ) )
74 3 67 71 72 73 cycpmrn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ran 𝑥 = dom ( ( 𝑀 ‘ 𝑥 ) ∖ I ) )
75 55 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 : dom 𝑠 –1-1→ 𝐷 )
76 6 ssdifd ⊢ ( 𝜑 → ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ⊆ ( dom 𝑀 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
77 76 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑠 ∈ ( dom 𝑀 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
78 77 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 ∈ ( dom 𝑀 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
79 78 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ¬ 𝑠 ∈ ( ◡ ♯ “ { 0 , 1 } ) )
80 hashgt1 ⊢ ( 𝑠 ∈ 𝐴 → ( ¬ 𝑠 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ 1 < ( ♯ ‘ 𝑠 ) ) )
81 80 biimpa ⊢ ( ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ∈ ( ◡ ♯ “ { 0 , 1 } ) ) → 1 < ( ♯ ‘ 𝑠 ) )
82 48 79 81 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 1 < ( ♯ ‘ 𝑠 ) )
83 3 67 56 75 82 cycpmrn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ran 𝑠 = dom ( ( 𝑀 ‘ 𝑠 ) ∖ I ) )
84 66 74 83 3eqtr4rd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ran 𝑠 = ran 𝑥 )
85 84 ineq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ran 𝑥 ∩ ran 𝑠 ) = ( ran 𝑥 ∩ ran 𝑥 ) )
86 inidm ⊢ ( ran 𝑥 ∩ ran 𝑥 ) = ran 𝑥
87 85 86 eqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ran 𝑥 ∩ ran 𝑠 ) = ran 𝑥 )
88 rneq ⊢ ( 𝑥 = 𝑦 → ran 𝑥 = ran 𝑦 )
89 88 cbvdisjv ⊢ ( Disj 𝑥 ∈ 𝐴 ran 𝑥 ↔ Disj 𝑦 ∈ 𝐴 ran 𝑦 )
90 5 89 sylib ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 ran 𝑦 )
91 90 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → Disj 𝑦 ∈ 𝐴 ran 𝑦 )
92 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ¬ 𝑠 = 𝑥 )
93 92 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 ≠ 𝑥 )
94 93 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 ≠ 𝑠 )
95 rneq ⊢ ( 𝑦 = 𝑥 → ran 𝑦 = ran 𝑥 )
96 rneq ⊢ ( 𝑦 = 𝑠 → ran 𝑦 = ran 𝑠 )
97 95 96 disji2 ⊢ ( ( Disj 𝑦 ∈ 𝐴 ran 𝑦 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑠 ) → ( ran 𝑥 ∩ ran 𝑠 ) = ∅ )
98 91 68 48 94 97 syl121anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ( ran 𝑥 ∩ ran 𝑠 ) = ∅ )
99 87 98 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ran 𝑥 = ∅ )
100 84 99 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → ran 𝑠 = ∅ )
101 relrn0 ⊢ ( Rel 𝑠 → ( 𝑠 = ∅ ↔ ran 𝑠 = ∅ ) )
102 101 biimpar ⊢ ( ( Rel 𝑠 ∧ ran 𝑠 = ∅ ) → 𝑠 = ∅ )
103 59 100 102 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 = ∅ )
104 wrdf ⊢ ( 𝑥 ∈ Word 𝐷 → 𝑥 : ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⟶ 𝐷 )
105 frel ⊢ ( 𝑥 : ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⟶ 𝐷 → Rel 𝑥 )
106 71 104 105 3syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → Rel 𝑥 )
107 relrn0 ⊢ ( Rel 𝑥 → ( 𝑥 = ∅ ↔ ran 𝑥 = ∅ ) )
108 107 biimpar ⊢ ( ( Rel 𝑥 ∧ ran 𝑥 = ∅ ) → 𝑥 = ∅ )
109 106 99 108 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑥 = ∅ )
110 103 109 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) ∧ ¬ 𝑠 = 𝑥 ) → 𝑠 = 𝑥 )
111 110 pm2.18da ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) → 𝑠 = 𝑥 )
112 111 ex ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) → 𝑠 = 𝑥 ) )
113 112 anasss ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) → ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) → 𝑠 = 𝑥 ) )
114 113 ralrimivva ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ∀ 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑠 ) = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) → 𝑠 = 𝑥 ) )
115 dff13 ⊢ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 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 ⊢ ( 𝜑 → ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1→ ( Base ‘ 𝑆 ) )
117 f1f1orn ⊢ ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1→ ( Base ‘ 𝑆 ) → ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1-onto→ ran ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) )
118 116 117 syl ⊢ ( 𝜑 → ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1-onto→ ran ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) )
119 df-ima ⊢ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) = ran ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) )
120 119 a1i ⊢ ( 𝜑 → ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) = ran ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) )
121 120 f1oeq3d ⊢ ( 𝜑 → ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1-onto→ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ↔ ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1-onto→ ran ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) )
122 118 121 mpbird ⊢ ( 𝜑 → ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) : ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) –1-1-onto→ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) )
123 simpr ⊢ ( ( 𝜑 ∧ 𝑐 = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) → 𝑐 = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) )
124 123 difeq1d ⊢ ( ( 𝜑 ∧ 𝑐 = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) → ( 𝑐 ∖ I ) = ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) )
125 124 dmeqd ⊢ ( ( 𝜑 ∧ 𝑐 = ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ) → dom ( 𝑐 ∖ I ) = dom ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) )
126 122 125 disjrdx ⊢ ( 𝜑 → ( Disj 𝑥 ∈ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) dom ( ( ( 𝑀 ↾ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ‘ 𝑥 ) ∖ I ) ↔ Disj 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) dom ( 𝑐 ∖ I ) ) )
127 40 126 mpbid ⊢ ( 𝜑 → Disj 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) dom ( 𝑐 ∖ I ) )
128 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → ( 𝑀 ‘ 𝑥 ) = 𝑐 )
129 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → 𝐷 ∈ 𝑉 )
130 6 ssrind ⊢ ( 𝜑 → ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ⊆ ( dom 𝑀 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) )
131 130 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ⊆ ( dom 𝑀 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) )
132 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) )
133 131 132 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → 𝑥 ∈ ( dom 𝑀 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) )
134 3 tocyc01 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑥 ∈ ( dom 𝑀 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝑀 ‘ 𝑥 ) = ( I ↾ 𝐷 ) )
135 129 133 134 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → ( 𝑀 ‘ 𝑥 ) = ( I ↾ 𝐷 ) )
136 128 135 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → 𝑐 = ( I ↾ 𝐷 ) )
137 136 difeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → ( 𝑐 ∖ I ) = ( ( I ↾ 𝐷 ) ∖ I ) )
138 137 dmeqd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → dom ( 𝑐 ∖ I ) = dom ( ( I ↾ 𝐷 ) ∖ I ) )
139 resdifcom ⊢ ( ( I ↾ 𝐷 ) ∖ I ) = ( ( I ∖ I ) ↾ 𝐷 )
140 difid ⊢ ( I ∖ I ) = ∅
141 140 reseq1i ⊢ ( ( I ∖ I ) ↾ 𝐷 ) = ( ∅ ↾ 𝐷 )
142 0res ⊢ ( ∅ ↾ 𝐷 ) = ∅
143 139 141 142 3eqtri ⊢ ( ( I ↾ 𝐷 ) ∖ I ) = ∅
144 143 dmeqi ⊢ dom ( ( I ↾ 𝐷 ) ∖ I ) = dom ∅
145 dm0 ⊢ dom ∅ = ∅
146 144 145 eqtri ⊢ dom ( ( I ↾ 𝐷 ) ∖ I ) = ∅
147 138 146 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( 𝑀 ‘ 𝑥 ) = 𝑐 ) → dom ( 𝑐 ∖ I ) = ∅ )
148 41 ffund ⊢ ( 𝜑 → Fun 𝑀 )
149 fvelima ⊢ ( ( Fun 𝑀 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ( 𝑀 ‘ 𝑥 ) = 𝑐 )
150 148 149 sylan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ( 𝑀 ‘ 𝑥 ) = 𝑐 )
151 147 150 r19.29a ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) → dom ( 𝑐 ∖ I ) = ∅ )
152 151 disjxun0 ⊢ ( 𝜑 → ( Disj 𝑐 ∈ ( ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) dom ( 𝑐 ∖ I ) ↔ Disj 𝑐 ∈ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) dom ( 𝑐 ∖ I ) ) )
153 127 152 mpbird ⊢ ( 𝜑 → Disj 𝑐 ∈ ( ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) dom ( 𝑐 ∖ I ) )
154 uncom ⊢ ( ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) = ( ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) )
155 imaundi ⊢ ( 𝑀 “ ( ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ∪ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) = ( ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) )
156 inundif ⊢ ( ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ∪ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) = 𝐴
157 156 imaeq2i ⊢ ( 𝑀 “ ( ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ∪ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) = ( 𝑀 “ 𝐴 )
158 154 155 157 3eqtr2i ⊢ ( ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) = ( 𝑀 “ 𝐴 )
159 158 a1i ⊢ ( 𝜑 → ( ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) = ( 𝑀 “ 𝐴 ) )
160 159 disjeq1d ⊢ ( 𝜑 → ( Disj 𝑐 ∈ ( ( 𝑀 “ ( 𝐴 ∖ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∪ ( 𝑀 “ ( 𝐴 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ) dom ( 𝑐 ∖ I ) ↔ Disj 𝑐 ∈ ( 𝑀 “ 𝐴 ) dom ( 𝑐 ∖ I ) ) )
161 153 160 mpbid ⊢ ( 𝜑 → Disj 𝑐 ∈ ( 𝑀 “ 𝐴 ) dom ( 𝑐 ∖ I ) )
162 1 7 2 10 161 symgcntz ⊢ ( 𝜑 → ( 𝑀 “ 𝐴 ) ⊆ ( 𝑍 ‘ ( 𝑀 “ 𝐴 ) ) )