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
|
syl5bb |
⊢ ( 𝑦 ∈ { 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 |
171
|
raleqdv |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ) ) |
173 |
170 172
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ) |
174 |
|
prex |
⊢ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ∈ V |
175 |
135 174
|
unex |
⊢ ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ∈ V |
176 |
|
f1oeq1 |
⊢ ( 𝑓 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) ) |
177 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) |
178 |
177
|
neeq1d |
⊢ ( 𝑓 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ) ) |
179 |
178
|
ralbidv |
⊢ ( 𝑓 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ) ) |
180 |
176 179
|
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 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ) ) ) |
181 |
175 180 3
|
elab2 |
⊢ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ∈ 𝐴 ↔ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ≠ 𝑦 ) ) |
182 |
145 173 181
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ∈ 𝐴 ) |
183 |
151 158
|
jca |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) = 1 ) ) |
184 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( 𝑔 ‘ 1 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) ) |
185 |
184
|
eqeq1d |
⊢ ( 𝑔 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( ( 𝑔 ‘ 1 ) = 𝑀 ↔ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) = 𝑀 ) ) |
186 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( 𝑔 ‘ 𝑀 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) ) |
187 |
186
|
eqeq1d |
⊢ ( 𝑔 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( ( 𝑔 ‘ 𝑀 ) = 1 ↔ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) = 1 ) ) |
188 |
185 187
|
anbi12d |
⊢ ( 𝑔 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) → ( ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔 ‘ 𝑀 ) = 1 ) ↔ ( ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) = 1 ) ) ) |
189 |
188 8
|
elrab2 |
⊢ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ∈ 𝐵 ↔ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ∈ 𝐴 ∧ ( ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) = 𝑀 ∧ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) = 1 ) ) ) |
190 |
182 183 189
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ∈ 𝐵 ) |
191 |
57
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 1 ) = 𝑀 ) |
192 |
151
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) = 𝑀 ) |
193 |
191 192
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) ) |
194 |
60
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 𝑀 ) = 1 ) |
195 |
158
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) = 1 ) |
196 |
194 195
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ‘ 𝑀 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) ) |
197 |
|
fveq2 |
⊢ ( 𝑦 = 1 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 1 ) ) |
198 |
197 161
|
eqeq12d |
⊢ ( 𝑦 = 1 → ( ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) ) ) |
199 |
|
fveq2 |
⊢ ( 𝑦 = 𝑀 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑀 ) ) |
200 |
199 164
|
eqeq12d |
⊢ ( 𝑦 = 𝑀 → ( ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑀 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) ) ) |
201 |
61 6 198 200
|
ralpr |
⊢ ( ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ( ( 𝑏 ‘ 1 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 1 ) ∧ ( 𝑏 ‘ 𝑀 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑀 ) ) ) |
202 |
193 196 201
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) |
203 |
202
|
biantrud |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) ) ) |
204 |
|
ralunb |
⊢ ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { 1 , 𝑀 } ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) ) |
205 |
203 204
|
bitr4di |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) ) |
206 |
146
|
eqeq2d |
⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) |
207 |
206
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) |
208 |
207
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) |
209 |
52
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ) |
210 |
209
|
raleqdv |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) ) |
211 |
205 208 210
|
3bitr3rd |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) |
212 |
124
|
eqeq2d |
⊢ ( 𝑦 ∈ 𝐾 → ( ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ↔ ( 𝑐 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) ) |
213 |
|
eqcom |
⊢ ( ( 𝑐 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) |
214 |
212 213
|
bitrdi |
⊢ ( 𝑦 ∈ 𝐾 → ( ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) |
215 |
214
|
ralbiia |
⊢ ( ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) |
216 |
211 215
|
bitr4di |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ) ) |
217 |
43
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) ) |
218 |
145
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) |
219 |
|
f1ofn |
⊢ ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) Fn ( 1 ... ( 𝑁 + 1 ) ) ) |
220 |
218 219
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) Fn ( 1 ... ( 𝑁 + 1 ) ) ) |
221 |
|
eqfnfv |
⊢ ( ( 𝑏 Fn ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) Fn ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑏 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) ) |
222 |
217 220 221
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑏 ‘ 𝑦 ) = ( ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ‘ 𝑦 ) ) ) |
223 |
143
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 : 𝐾 –1-1-onto→ 𝐾 ) |
224 |
|
f1ofn |
⊢ ( 𝑐 : 𝐾 –1-1-onto→ 𝐾 → 𝑐 Fn 𝐾 ) |
225 |
223 224
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 Fn 𝐾 ) |
226 |
116
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐾 ⊆ ( 1 ... ( 𝑁 + 1 ) ) ) |
227 |
217 226
|
fnssresd |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ↾ 𝐾 ) Fn 𝐾 ) |
228 |
|
eqfnfv |
⊢ ( ( 𝑐 Fn 𝐾 ∧ ( 𝑏 ↾ 𝐾 ) Fn 𝐾 ) → ( 𝑐 = ( 𝑏 ↾ 𝐾 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ) ) |
229 |
225 227 228
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑐 = ( 𝑏 ↾ 𝐾 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑐 ‘ 𝑦 ) = ( ( 𝑏 ↾ 𝐾 ) ‘ 𝑦 ) ) ) |
230 |
216 222 229
|
3bitr4d |
⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 = ( 𝑐 ∪ { 〈 1 , 𝑀 〉 , 〈 𝑀 , 1 〉 } ) ↔ 𝑐 = ( 𝑏 ↾ 𝐾 ) ) ) |
231 |
19 130 190 230
|
f1o2d |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ↾ 𝐾 ) ) : 𝐵 –1-1-onto→ 𝐶 ) |
232 |
18 231
|
hasheqf1od |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐶 ) ) |
233 |
9
|
fveq2i |
⊢ ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) |
234 |
|
fzfi |
⊢ ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin |
235 |
|
diffi |
⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∈ Fin → ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin ) |
236 |
234 235
|
ax-mp |
⊢ ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } ) ∈ Fin |
237 |
7 236
|
eqeltri |
⊢ 𝐾 ∈ Fin |
238 |
1
|
derangval |
⊢ ( 𝐾 ∈ Fin → ( 𝐷 ‘ 𝐾 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ) |
239 |
237 238
|
ax-mp |
⊢ ( 𝐷 ‘ 𝐾 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝐾 –1-1-onto→ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) |
240 |
1 2
|
derangen2 |
⊢ ( 𝐾 ∈ Fin → ( 𝐷 ‘ 𝐾 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) ) |
241 |
237 240
|
ax-mp |
⊢ ( 𝐷 ‘ 𝐾 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) |
242 |
233 239 241
|
3eqtr2ri |
⊢ ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) = ( ♯ ‘ 𝐶 ) |
243 |
51
|
simp3d |
⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) |
244 |
243
|
fveq2d |
⊢ ( 𝜑 → ( 𝑆 ‘ ( ♯ ‘ 𝐾 ) ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) ) |
245 |
242 244
|
eqtr3id |
⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) ) |
246 |
232 245
|
eqtrd |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑆 ‘ ( 𝑁 − 1 ) ) ) |