Metamath Proof Explorer

Theorem subfacp1lem3

Description: Lemma for subfacp1 . In subfacp1lem6 we cut up the set of all derangements on 1 ... ( N + 1 ) first according to the value at 1 , and then by whether or not ( f( f1 ) ) = 1 . In this lemma, we show that the subset of all N + 1 derangements that satisfy this for fixed M = ( f1 ) is in bijection with N - 1 derangements, by simply dropping the x = 1 and x = M points from the function to get a derangement on K = ( 1 ... ( N - 1 ) ) \ { 1 , M } . (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Hypotheses derang.d ⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
subfac.n ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
subfacp1lem.a ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
subfacp1lem1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
subfacp1lem1.m ⊢ ( 𝜑 → 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
subfacp1lem1.x ⊢ 𝑀 ∈ V
subfacp1lem1.k ⊢ 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
subfacp1lem3.b ⊢ 𝐵 = { 𝑔 ∈ 𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) = 1 ) }
subfacp1lem3.c ⊢ 𝐶 = { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
Assertion subfacp1lem3 ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 derang.d ⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2 subfac.n ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3 subfacp1lem.a ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
4 subfacp1lem1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 subfacp1lem1.m ⊢ ( 𝜑 → 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
6 subfacp1lem1.x ⊢ 𝑀 ∈ V
7 subfacp1lem1.k ⊢ 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
8 subfacp1lem3.b ⊢ 𝐵 = { 𝑔 ∈ 𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) = 1 ) }
9 subfacp1lem3.c ⊢ 𝐶 = { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
10 fzfi ⊢ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin
11 deranglem ⊢ ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin → { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin )
12 10 11 ax-mp ⊢ { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin
13 3 12 eqeltri ⊢ 𝐴 ∈ Fin
14 8 ssrab3 ⊢ 𝐵 ⊆ 𝐴
15 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )
16 13 14 15 mp2an ⊢ 𝐵 ∈ Fin
17 16 elexi ⊢ 𝐵 ∈ V
18 17 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
19 eqid ⊢ ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ↾ 𝐾 ) ) = ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ↾ 𝐾 ) )
20 fveq1 ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ‘ 1 ) = ( 𝑏 ‘ 1 ) )
21 20 eqeq1d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( 𝑏 ‘ 1 ) = 𝑀 ) )
22 fveq1 ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ‘ 𝑀 ) = ( 𝑏 ‘ 𝑀 ) )
23 22 eqeq1d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑔 ‘ 𝑀 ) = 1 ↔ ( 𝑏 ‘ 𝑀 ) = 1 ) )
24 21 23 anbi12d ⊢ ( 𝑔 = 𝑏 → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) = 1 ) ↔ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) = 1 ) ) )
25 24 8 elrab2 ⊢ ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) = 1 ) ) )
26 25 bilani ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐴 ∧ ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) = 1 ) ) )
27 26 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐴 )
28 vex ⊢ 𝑏 ∈ V
29 f1oeq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
30 fveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
31 30 neeq1d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
32 31 ralbidv ⊢ ( 𝑓 = 𝑏 → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
33 29 32 anbi12d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) ) )
34 28 33 3 elab2 ⊢ ( 𝑏 ∈ 𝐴 ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
35 27 34 sylib ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
36 35 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
37 f1of1 ⊢ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) )
38 df-f1 ⊢ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) ∧ Fun ◡ 𝑏 ) )
39 38 simprbi ⊢ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ ( 1 ... ( 𝑁 + 1 ) ) → Fun ◡ 𝑏 )
40 36 37 39 3syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Fun ◡ 𝑏 )
41 f1ofn ⊢ ( 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) )
42 36 41 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) )
43 fnresdm ⊢ ( 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) = 𝑏 )
44 f1oeq1 ⊢ ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) = 𝑏 → ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
45 42 43 44 3syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑏 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
46 36 45 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
47 f1ofo ⊢ ( ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) )
49 ssun2 ⊢ { 1 , 𝑀 } ⊆ ( 𝐾 ∪ { 1 , 𝑀 } )
50 1 2 3 4 5 6 7 subfacp1lem1 ⊢ ( 𝜑 → ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) )
51 50 simp2d ⊢ ( 𝜑 → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
52 49 51 sseqtrid ⊢ ( 𝜑 → { 1 , 𝑀 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → { 1 , 𝑀 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
54 42 53 fnssresd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ { 1 , 𝑀 } ) Fn { 1 , 𝑀 } )
55 26 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) = 𝑀 ∧ ( 𝑏 ‘ 𝑀 ) = 1 ) )
56 55 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) = 𝑀 )
57 6 prid2 ⊢ 𝑀 ∈ { 1 , 𝑀 }
58 56 57 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) ∈ { 1 , 𝑀 } )
59 55 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝑀 ) = 1 )
60 1ex ⊢ 1 ∈ V
61 60 prid1 ⊢ 1 ∈ { 1 , 𝑀 }
62 59 61 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝑀 ) ∈ { 1 , 𝑀 } )
63 fveq2 ⊢ ( 𝑥 = 1 → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ 1 ) )
64 63 eleq1d ⊢ ( 𝑥 = 1 → ( ( 𝑏 ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ( 𝑏 ‘ 1 ) ∈ { 1 , 𝑀 } ) )
65 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑀 ) )
66 65 eleq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑏 ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ( 𝑏 ‘ 𝑀 ) ∈ { 1 , 𝑀 } ) )
67 60 6 64 66 ralpr ⊢ ( ∀ 𝑥 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ( ( 𝑏 ‘ 1 ) ∈ { 1 , 𝑀 } ∧ ( 𝑏 ‘ 𝑀 ) ∈ { 1 , 𝑀 } ) )
68 58 62 67 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑥 ) ∈ { 1 , 𝑀 } )
69 fvres ⊢ ( 𝑥 ∈ { 1 , 𝑀 } → ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
70 69 eleq1d ⊢ ( 𝑥 ∈ { 1 , 𝑀 } → ( ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ( 𝑏 ‘ 𝑥 ) ∈ { 1 , 𝑀 } ) )
71 70 ralbiia ⊢ ( ∀ 𝑥 ∈ { 1 , 𝑀 } ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } ↔ ∀ 𝑥 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑥 ) ∈ { 1 , 𝑀 } )
72 68 71 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } )
73 ffnfv ⊢ ( ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } ⟶ { 1 , 𝑀 } ↔ ( ( 𝑏 ↾ { 1 , 𝑀 } ) Fn { 1 , 𝑀 } ∧ ∀ 𝑥 ∈ { 1 , 𝑀 } ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑥 ) ∈ { 1 , 𝑀 } ) )
74 54 72 73 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } ⟶ { 1 , 𝑀 } )
75 fveqeq2 ⊢ ( 𝑦 = 𝑀 → ( ( 𝑏 ‘ 𝑦 ) = 1 ↔ ( 𝑏 ‘ 𝑀 ) = 1 ) )
76 75 rspcev ⊢ ( ( 𝑀 ∈ { 1 , 𝑀 } ∧ ( 𝑏 ‘ 𝑀 ) = 1 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 1 )
77 57 59 76 sylancr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 1 )
78 fveqeq2 ⊢ ( 𝑦 = 1 → ( ( 𝑏 ‘ 𝑦 ) = 𝑀 ↔ ( 𝑏 ‘ 1 ) = 𝑀 ) )
79 78 rspcev ⊢ ( ( 1 ∈ { 1 , 𝑀 } ∧ ( 𝑏 ‘ 1 ) = 𝑀 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑀 )
80 61 56 79 sylancr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑀 )
81 eqeq2 ⊢ ( 𝑥 = 1 → ( ( 𝑏 ‘ 𝑦 ) = 𝑥 ↔ ( 𝑏 ‘ 𝑦 ) = 1 ) )
82 81 rexbidv ⊢ ( 𝑥 = 1 → ( ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 1 ) )
83 eqeq2 ⊢ ( 𝑥 = 𝑀 → ( ( 𝑏 ‘ 𝑦 ) = 𝑥 ↔ ( 𝑏 ‘ 𝑦 ) = 𝑀 ) )
84 83 rexbidv ⊢ ( 𝑥 = 𝑀 → ( ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑀 ) )
85 60 6 82 84 ralpr ⊢ ( ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑥 ↔ ( ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 1 ∧ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑀 ) )
86 77 80 85 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑥 )
87 eqcom ⊢ ( 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) = 𝑥 )
88 fvres ⊢ ( 𝑦 ∈ { 1 , 𝑀 } → ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
89 88 eqeq1d ⊢ ( 𝑦 ∈ { 1 , 𝑀 } → ( ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) = 𝑥 ↔ ( 𝑏 ‘ 𝑦 ) = 𝑥 ) )
90 87 89 bitrid ⊢ ( 𝑦 ∈ { 1 , 𝑀 } → ( 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = 𝑥 ) )
91 90 rexbiia ⊢ ( ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑥 )
92 91 ralbii ⊢ ( ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = 𝑥 )
93 86 92 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) )
94 dffo3 ⊢ ( ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } –onto→ { 1 , 𝑀 } ↔ ( ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } ⟶ { 1 , 𝑀 } ∧ ∀ 𝑥 ∈ { 1 , 𝑀 } ∃ 𝑦 ∈ { 1 , 𝑀 } 𝑥 = ( ( 𝑏 ↾ { 1 , 𝑀 } ) ‘ 𝑦 ) ) )
95 74 93 94 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } –onto→ { 1 , 𝑀 } )
96 resdif ⊢ ( ( Fun ◡ 𝑏 ∧ ( 𝑏 ↾ ( 1 ... ( 𝑁 + 1 ) ) ) : ( 1 ... ( 𝑁 + 1 ) ) –onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑏 ↾ { 1 , 𝑀 } ) : { 1 , 𝑀 } –onto→ { 1 , 𝑀 } ) → ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) )
97 40 48 95 96 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) )
98 uncom ⊢ ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 𝐾 ∪ { 1 , 𝑀 } )
99 98 51 eqtrid ⊢ ( 𝜑 → ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 1 ... ( 𝑁 + 1 ) ) )
100 incom ⊢ ( { 1 , 𝑀 } ∩ 𝐾 ) = ( 𝐾 ∩ { 1 , 𝑀 } )
101 50 simp1d ⊢ ( 𝜑 → ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ )
102 100 101 eqtrid ⊢ ( 𝜑 → ( { 1 , 𝑀 } ∩ 𝐾 ) = ∅ )
103 uneqdifeq ⊢ ( ( { 1 , 𝑀 } ⊆ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( { 1 , 𝑀 } ∩ 𝐾 ) = ∅ ) → ( ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 ) )
104 52 102 103 syl2anc ⊢ ( 𝜑 → ( ( { 1 , 𝑀 } ∪ 𝐾 ) = ( 1 ... ( 𝑁 + 1 ) ) ↔ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 ) )
105 99 104 mpbid ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 )
107 reseq2 ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) = ( 𝑏 ↾ 𝐾 ) )
108 107 f1oeq1d ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏 ↾ 𝐾 ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) )
109 f1oeq2 ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏 ↾ 𝐾 ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) )
110 f1oeq3 ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 ) )
111 108 109 110 3bitrd ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) = 𝐾 → ( ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 ) )
112 106 111 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ↾ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ) : ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) –1-1-onto→ ( ( 1 ... ( 𝑁 + 1 ) ) ∖ { 1 , 𝑀 } ) ↔ ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 ) )
113 97 112 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 )
114 ssun1 ⊢ 𝐾 ⊆ ( 𝐾 ∪ { 1 , 𝑀 } )
115 114 51 sseqtrid ⊢ ( 𝜑 → 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
117 35 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 )
118 ssralv ⊢ ( 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 → ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
119 116 117 118 sylc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 )
120 28 resex ⊢ ( 𝑏 ↾ 𝐾 ) ∈ V
121 f1oeq1 ⊢ ( 𝑓 = ( 𝑏 ↾ 𝐾 ) → ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ↔ ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 ) )
122 fveq1 ⊢ ( 𝑓 = ( 𝑏 ↾ 𝐾 ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) )
123 fvres ⊢ ( 𝑦 ∈ 𝐾 → ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
124 122 123 sylan9eq ⊢ ( ( 𝑓 = ( 𝑏 ↾ 𝐾 ) ∧ 𝑦 ∈ 𝐾 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
125 124 neeq1d ⊢ ( ( 𝑓 = ( 𝑏 ↾ 𝐾 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
126 125 ralbidva ⊢ ( 𝑓 = ( 𝑏 ↾ 𝐾 ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
127 121 126 anbi12d ⊢ ( 𝑓 = ( 𝑏 ↾ 𝐾 ) → ( ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) ) )
128 120 127 9 elab2 ⊢ ( ( 𝑏 ↾ 𝐾 ) ∈ 𝐶 ↔ ( ( 𝑏 ↾ 𝐾 ) : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) ≠ 𝑦 ) )
129 113 119 128 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ↾ 𝐾 ) ∈ 𝐶 )
130 4 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑁 ∈ ℕ )
131 5 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
132 eqid ⊢ ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
133 vex ⊢ 𝑐 ∈ V
134 f1oeq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ↔ 𝑐 : 𝐾 –1-1-onto→ 𝐾 ) )
135 fveq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
136 135 neeq1d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
137 136 ralbidv ⊢ ( 𝑓 = 𝑐 → ( ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
138 134 137 anbi12d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( 𝑐 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) ) )
139 133 138 9 elab2 ⊢ ( 𝑐 ∈ 𝐶 ↔ ( 𝑐 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
140 139 bilani ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 ) )
141 140 simpld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 : 𝐾 –1-1-onto→ 𝐾 )
142 1 2 3 130 131 6 7 132 141 subfacp1lem2a ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) )
143 142 simp1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
144 1 2 3 130 131 6 7 132 141 subfacp1lem2b ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
145 140 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 )
146 145 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐾 ) → ( 𝑐 ‘ 𝑦 ) ≠ 𝑦 )
147 144 146 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
148 147 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ 𝐾 ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
149 142 simp2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 )
150 elfzuz ⊢ ( 𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
151 eluz2b3 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
152 151 simprbi ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ≠ 1 )
153 5 150 152 3syl ⊢ ( 𝜑 → 𝑀 ≠ 1 )
154 153 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 𝑀 ≠ 1 )
155 149 154 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ≠ 1 )
156 142 simp3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 )
157 154 necomd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → 1 ≠ 𝑀 )
158 156 157 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ≠ 𝑀 )
159 fveq2 ⊢ ( 𝑦 = 1 → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) )
160 id ⊢ ( 𝑦 = 1 → 𝑦 = 1 )
161 159 160 neeq12d ⊢ ( 𝑦 = 1 → ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ≠ 1 ) )
162 fveq2 ⊢ ( 𝑦 = 𝑀 → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) )
163 id ⊢ ( 𝑦 = 𝑀 → 𝑦 = 𝑀 )
164 162 163 neeq12d ⊢ ( 𝑦 = 𝑀 → ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ≠ 𝑀 ) )
165 60 6 161 164 ralpr ⊢ ( ∀ 𝑦 ∈ { 1 , 𝑀 } ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ≠ 1 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ≠ 𝑀 ) )
166 155 158 165 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ { 1 , 𝑀 } ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
167 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ( ∀ 𝑦 ∈ 𝐾 ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
168 148 166 167 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
169 51 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
170 168 169 raleqtrdv ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 )
171 prex ⊢ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ∈ V
172 133 171 unex ⊢ ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ V
173 f1oeq1 ⊢ ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
174 fveq1 ⊢ ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) )
175 174 neeq1d ⊢ ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
176 175 ralbidv ⊢ ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
177 173 176 anbi12d ⊢ ( 𝑓 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) ) )
178 172 177 3 elab2 ⊢ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐴 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ≠ 𝑦 ) )
179 143 170 178 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐴 )
180 149 156 jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) )
181 fveq1 ⊢ ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑔 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) )
182 181 eqeq1d ⊢ ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ) )
183 fveq1 ⊢ ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝑔 ‘ 𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) )
184 183 eqeq1d ⊢ ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( 𝑔 ‘ 𝑀 ) = 1 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) )
185 182 184 anbi12d ⊢ ( 𝑔 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) = 1 ) ↔ ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) ) )
186 185 8 elrab2 ⊢ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐵 ↔ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐴 ∧ ( ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 ) ) )
187 179 180 186 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ∈ 𝐵 )
188 56 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 1 ) = 𝑀 )
189 149 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) = 𝑀 )
190 188 189 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) )
191 59 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 𝑀 ) = 1 )
192 156 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) = 1 )
193 191 192 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) )
194 fveq2 ⊢ ( 𝑦 = 1 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 1 ) )
195 194 159 eqeq12d ⊢ ( 𝑦 = 1 → ( ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ) )
196 fveq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑀 ) )
197 196 162 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ) )
198 60 6 195 197 ralpr ⊢ ( ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 1 ) ∧ ( 𝑏 ‘ 𝑀 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑀 ) ) )
199 190 193 198 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) )
200 199 biantrud ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) ) )
201 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
202 200 201 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
203 144 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
204 203 ralbidva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
205 204 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
206 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
207 206 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
208 202 205 207 3bitr3rd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
209 123 eqeq2d ⊢ ( 𝑦 ∈ 𝐾 → ( ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ↔ ( 𝑐 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) )
210 eqcom ⊢ ( ( 𝑐 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
211 209 210 bitrdi ⊢ ( 𝑦 ∈ 𝐾 → ( ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) )
212 211 ralbiia ⊢ ( ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) )
213 208 212 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ) )
214 42 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) )
215 143 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
216 f1ofn ⊢ ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
217 215 216 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) Fn ( 1 ... ( 𝑁 + 1 ) ) )
218 eqfnfv ⊢ ( ( 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) Fn ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
219 214 217 218 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ‘ 𝑦 ) ) )
220 141 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 : 𝐾 –1-1-onto→ 𝐾 )
221 f1ofn ⊢ ( 𝑐 : 𝐾 –1-1-onto→ 𝐾 → 𝑐 Fn 𝐾 )
222 220 221 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 Fn 𝐾 )
223 115 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
224 214 223 fnssresd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ↾ 𝐾 ) Fn 𝐾 )
225 eqfnfv ⊢ ( ( 𝑐 Fn 𝐾 ∧ ( 𝑏 ↾ 𝐾 ) Fn 𝐾 ) → ( 𝑐 = ( 𝑏 ↾ 𝐾 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ) )
226 222 224 225 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑐 = ( 𝑏 ↾ 𝐾 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ) )
227 213 219 226 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 = ( 𝑐 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) ↔ 𝑐 = ( 𝑏 ↾ 𝐾 ) ) )
228 19 129 187 227 f1o2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ↾ 𝐾 ) ) : 𝐵 –1-1-onto→ 𝐶 )
229 18 228 hasheqf1od ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐶 ) )
230 9 fveq2i ⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } )
231 fzfi ⊢ ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin
232 diffi ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin )
233 231 232 ax-mp ⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin
234 7 233 eqeltri ⊢ 𝐾 ∈ Fin
235 1 derangval ⊢ ( 𝐾 ∈ Fin → ( 𝐷 ‘ 𝐾 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
236 234 235 ax-mp ⊢ ( 𝐷 ‘ 𝐾 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } )
237 1 2 derangen2 ⊢ ( 𝐾 ∈ Fin → ( 𝐷 ‘ 𝐾 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) )
238 234 237 ax-mp ⊢ ( 𝐷 ‘ 𝐾 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) )
239 230 236 238 3eqtr2ri ⊢ ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) = ( ♯ ‘ 𝐶 )
240 50 simp3d ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) )
241 240 fveq2d ⊢ ( 𝜑 → ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )
242 239 241 eqtr3id ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )
243 229 242 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) )