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