Metamath Proof Explorer


Theorem poimirlem9

Description: Lemma for poimir , establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
poimirlem9.1 φ T S
poimirlem9.2 φ 2 nd T 1 N 1
poimirlem9.3 φ U S
poimirlem9.4 φ 2 nd 1 st U 2 nd 1 st T
Assertion poimirlem9 φ 2 nd 1 st U = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T I 1 N 2 nd T 2 nd T + 1

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
3 poimirlem9.1 φ T S
4 poimirlem9.2 φ 2 nd T 1 N 1
5 poimirlem9.3 φ U S
6 poimirlem9.4 φ 2 nd 1 st U 2 nd 1 st T
7 resundi 2 nd 1 st U 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1
8 1 nncnd φ N
9 npcan1 N N - 1 + 1 = N
10 8 9 syl φ N - 1 + 1 = N
11 1 nnzd φ N
12 peano2zm N N 1
13 uzid N 1 N 1 N 1
14 peano2uz N 1 N 1 N - 1 + 1 N 1
15 11 12 13 14 4syl φ N - 1 + 1 N 1
16 10 15 eqeltrrd φ N N 1
17 fzss2 N N 1 1 N 1 1 N
18 16 17 syl φ 1 N 1 1 N
19 18 4 sseldd φ 2 nd T 1 N
20 fzp1elp1 2 nd T 1 N 1 2 nd T + 1 1 N - 1 + 1
21 4 20 syl φ 2 nd T + 1 1 N - 1 + 1
22 10 oveq2d φ 1 N - 1 + 1 = 1 N
23 21 22 eleqtrd φ 2 nd T + 1 1 N
24 19 23 prssd φ 2 nd T 2 nd T + 1 1 N
25 undif 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 1 N
26 24 25 sylib φ 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 1 N
27 26 reseq2d φ 2 nd 1 st U 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U 1 N
28 elrabi U t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
29 28 2 eleq2s U S U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
30 xp1st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
31 xp2nd 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st U f | f : 1 N 1-1 onto 1 N
32 5 29 30 31 4syl φ 2 nd 1 st U f | f : 1 N 1-1 onto 1 N
33 fvex 2 nd 1 st U V
34 f1oeq1 f = 2 nd 1 st U f : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N 1-1 onto 1 N
35 33 34 elab 2 nd 1 st U f | f : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N 1-1 onto 1 N
36 32 35 sylib φ 2 nd 1 st U : 1 N 1-1 onto 1 N
37 f1ofn 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U Fn 1 N
38 fnresdm 2 nd 1 st U Fn 1 N 2 nd 1 st U 1 N = 2 nd 1 st U
39 36 37 38 3syl φ 2 nd 1 st U 1 N = 2 nd 1 st U
40 27 39 eqtrd φ 2 nd 1 st U 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U
41 7 40 eqtr3id φ 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U
42 2lt3 2 < 3
43 2re 2
44 3re 3
45 43 44 ltnlei 2 < 3 ¬ 3 2
46 42 45 mpbi ¬ 3 2
47 df-pr 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T
48 47 coeq2i 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T
49 coundi 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T
50 48 49 eqtri 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T
51 elrabi T t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
52 51 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
53 xp1st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
54 xp2nd 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
55 3 52 53 54 4syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
56 fvex 2 nd 1 st T V
57 f1oeq1 f = 2 nd 1 st T f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
58 56 57 elab 2 nd 1 st T f | f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
59 55 58 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
60 f1of1 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 1 N
61 59 60 syl φ 2 nd 1 st T : 1 N 1-1 1 N
62 23 snssd φ 2 nd T + 1 1 N
63 f1ores 2 nd 1 st T : 1 N 1-1 1 N 2 nd T + 1 1 N 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1
64 61 62 63 syl2anc φ 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1
65 f1of 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 2 nd 1 st T 2 nd T + 1
66 64 65 syl φ 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 2 nd 1 st T 2 nd T + 1
67 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
68 59 67 syl φ 2 nd 1 st T Fn 1 N
69 fnsnfv 2 nd 1 st T Fn 1 N 2 nd T + 1 1 N 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T + 1
70 68 23 69 syl2anc φ 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T + 1
71 70 feq3d φ 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 2 nd 1 st T 2 nd T + 1
72 66 71 mpbird φ 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 2 nd 1 st T 2 nd T + 1
73 eqid 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
74 fvex 2 nd T V
75 ovex 2 nd T + 1 V
76 74 75 fsn 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
77 73 76 mpbir 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1
78 fco2 2 nd 1 st T 2 nd T + 1 : 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 : 2 nd T 2 nd 1 st T 2 nd T + 1
79 72 77 78 sylancl φ 2 nd 1 st T 2 nd T 2 nd T + 1 : 2 nd T 2 nd 1 st T 2 nd T + 1
80 fvex 2 nd 1 st T 2 nd T + 1 V
81 80 fconst2 2 nd 1 st T 2 nd T 2 nd T + 1 : 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd T × 2 nd 1 st T 2 nd T + 1
82 79 81 sylib φ 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd T × 2 nd 1 st T 2 nd T + 1
83 74 80 xpsn 2 nd T × 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T + 1
84 82 83 eqtrdi φ 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T + 1
85 84 uneq1d φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T
86 50 85 syl5eq φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T
87 elfznn 2 nd T 1 N 1 2 nd T
88 4 87 syl φ 2 nd T
89 88 nnred φ 2 nd T
90 89 ltp1d φ 2 nd T < 2 nd T + 1
91 89 90 ltned φ 2 nd T 2 nd T + 1
92 91 necomd φ 2 nd T + 1 2 nd T
93 f1veqaeq 2 nd 1 st T : 1 N 1-1 1 N 2 nd T + 1 1 N 2 nd T 1 N 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd T
94 61 23 19 93 syl12anc φ 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd T
95 94 necon3d φ 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
96 92 95 mpd φ 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
97 96 neneqd φ ¬ 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T
98 74 80 opth 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd T = 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T
99 98 simprbi 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T
100 97 99 nsyl φ ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T
101 91 neneqd φ ¬ 2 nd T = 2 nd T + 1
102 74 80 opth1 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd T + 1
103 101 102 nsyl φ ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
104 opex 2 nd T 2 nd 1 st T 2 nd T + 1 V
105 104 snid 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1
106 elun1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T
107 105 106 ax-mp 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T
108 eleq2 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
109 107 108 mpbii 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
110 104 elpr 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
111 oran 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1 ¬ ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
112 110 111 bitri 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 ¬ ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
113 109 112 sylib 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 ¬ ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
114 113 necon2ai ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T ¬ 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
115 100 103 114 syl2anc φ 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
116 86 115 eqnetrd φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
117 fnressn 2 nd 1 st T Fn 1 N 2 nd T 1 N 2 nd 1 st T 2 nd T = 2 nd T 2 nd 1 st T 2 nd T
118 68 19 117 syl2anc φ 2 nd 1 st T 2 nd T = 2 nd T 2 nd 1 st T 2 nd T
119 fnressn 2 nd 1 st T Fn 1 N 2 nd T + 1 1 N 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
120 68 23 119 syl2anc φ 2 nd 1 st T 2 nd T + 1 = 2 nd T + 1 2 nd 1 st T 2 nd T + 1
121 118 120 uneq12d φ 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
122 df-pr 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
123 122 reseq2i 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1
124 resundi 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
125 123 124 eqtri 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
126 df-pr 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
127 121 125 126 3eqtr4g φ 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1
128 1 2 3 4 5 poimirlem8 φ 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
129 uneq12 2 nd 1 st U 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
130 resundi 2 nd 1 st T 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
131 26 reseq2d φ 2 nd 1 st T 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N
132 fnresdm 2 nd 1 st T Fn 1 N 2 nd 1 st T 1 N = 2 nd 1 st T
133 59 67 132 3syl φ 2 nd 1 st T 1 N = 2 nd 1 st T
134 131 133 eqtrd φ 2 nd 1 st T 2 nd T 2 nd T + 1 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T
135 130 134 eqtr3id φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T
136 41 135 eqeq12d φ 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 2 nd 1 st U = 2 nd 1 st T
137 129 136 syl5ib φ 2 nd 1 st U 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 2 nd 1 st U = 2 nd 1 st T
138 128 137 mpan2d φ 2 nd 1 st U 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st U = 2 nd 1 st T
139 138 necon3d φ 2 nd 1 st U 2 nd 1 st T 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1
140 6 139 mpd φ 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1
141 140 necomd φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1
142 127 141 eqnetrrd φ 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1
143 prex 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T V
144 56 143 coex 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T V
145 prex 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 V
146 33 resex 2 nd 1 st U 2 nd T 2 nd T + 1 V
147 hashtpg 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T V 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 V 2 nd 1 st U 2 nd T 2 nd T + 1 V 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3
148 144 145 146 147 mp3an 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3
149 148 biimpi 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3
150 149 3expia 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3
151 116 142 150 syl2anc φ 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3
152 prex 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T V
153 prex 2 nd T 2 nd T + 1 V
154 152 153 mapval 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1 = f | f : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
155 prfi 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin
156 prfi 2 nd T 2 nd T + 1 Fin
157 mapfi 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin 2 nd T 2 nd T + 1 Fin 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1 Fin
158 155 156 157 mp2an 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1 Fin
159 154 158 eqeltrri f | f : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin
160 f1of f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
161 160 ss2abi f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
162 ssfi f | f : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin
163 159 161 162 mp2an f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin
164 23 19 prssd φ 2 nd T + 1 2 nd T 1 N
165 f1ores 2 nd 1 st T : 1 N 1-1 1 N 2 nd T + 1 2 nd T 1 N 2 nd 1 st T 2 nd T + 1 2 nd T : 2 nd T + 1 2 nd T 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd T
166 61 164 165 syl2anc φ 2 nd 1 st T 2 nd T + 1 2 nd T : 2 nd T + 1 2 nd T 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd T
167 fnimapr 2 nd 1 st T Fn 1 N 2 nd T + 1 1 N 2 nd T 1 N 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
168 68 23 19 167 syl3anc φ 2 nd 1 st T 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
169 168 f1oeq3d φ 2 nd 1 st T 2 nd T + 1 2 nd T : 2 nd T + 1 2 nd T 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T : 2 nd T + 1 2 nd T 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
170 166 169 mpbid φ 2 nd 1 st T 2 nd T + 1 2 nd T : 2 nd T + 1 2 nd T 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
171 f1oprg 2 nd T V 2 nd T + 1 V 2 nd T + 1 V 2 nd T V 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd T + 1 2 nd T
172 74 75 75 74 171 mp4an 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd T + 1 2 nd T
173 91 92 172 syl2anc φ 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd T + 1 2 nd T
174 f1oco 2 nd 1 st T 2 nd T + 1 2 nd T : 2 nd T + 1 2 nd T 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
175 170 173 174 syl2anc φ 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
176 rnpropg 2 nd T V 2 nd T + 1 V ran 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd T + 1 2 nd T
177 74 75 176 mp2an ran 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd T + 1 2 nd T
178 177 eqimssi ran 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T + 1 2 nd T
179 cores ran 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T
180 f1oeq1 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
181 178 179 180 mp2b 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
182 175 181 sylib φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
183 96 necomd φ 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
184 fvex 2 nd 1 st T 2 nd T V
185 f1oprg 2 nd T V 2 nd 1 st T 2 nd T V 2 nd T + 1 V 2 nd 1 st T 2 nd T + 1 V 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
186 74 184 75 80 185 mp4an 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
187 91 183 186 syl2anc φ 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
188 prcom 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
189 f1oeq3 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 = 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
190 188 189 ax-mp 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
191 187 190 sylib φ 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
192 f1of1 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N 1-1 1 N
193 36 192 syl φ 2 nd 1 st U : 1 N 1-1 1 N
194 f1ores 2 nd 1 st U : 1 N 1-1 1 N 2 nd T 2 nd T + 1 1 N 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st U 2 nd T 2 nd T + 1
195 193 24 194 syl2anc φ 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st U 2 nd T 2 nd T + 1
196 dff1o3 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N onto 1 N Fun 2 nd 1 st U -1
197 196 simprbi 2 nd 1 st U : 1 N 1-1 onto 1 N Fun 2 nd 1 st U -1
198 imadif Fun 2 nd 1 st U -1 2 nd 1 st U 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U 1 N 2 nd 1 st U 1 N 2 nd T 2 nd T + 1
199 36 197 198 3syl φ 2 nd 1 st U 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U 1 N 2 nd 1 st U 1 N 2 nd T 2 nd T + 1
200 f1ofo 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N onto 1 N
201 foima 2 nd 1 st U : 1 N onto 1 N 2 nd 1 st U 1 N = 1 N
202 36 200 201 3syl φ 2 nd 1 st U 1 N = 1 N
203 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
204 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
205 59 203 204 3syl φ 2 nd 1 st T 1 N = 1 N
206 202 205 eqtr4d φ 2 nd 1 st U 1 N = 2 nd 1 st T 1 N
207 128 rneqd φ ran 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = ran 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
208 df-ima 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = ran 2 nd 1 st U 1 N 2 nd T 2 nd T + 1
209 df-ima 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 = ran 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
210 207 208 209 3eqtr4g φ 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
211 206 210 difeq12d φ 2 nd 1 st U 1 N 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
212 dff1o3 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N Fun 2 nd 1 st T -1
213 212 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
214 imadif Fun 2 nd 1 st T -1 2 nd 1 st T 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
215 59 213 214 3syl φ 2 nd 1 st T 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
216 dfin4 1 N 2 nd T 2 nd T + 1 = 1 N 1 N 2 nd T 2 nd T + 1
217 sseqin2 2 nd T 2 nd T + 1 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
218 24 217 sylib φ 1 N 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
219 216 218 eqtr3id φ 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
220 219 imaeq2d φ 2 nd 1 st T 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1
221 215 220 eqtr3d φ 2 nd 1 st T 1 N 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1
222 199 211 221 3eqtrd φ 2 nd 1 st U 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1
223 219 imaeq2d φ 2 nd 1 st U 1 N 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st U 2 nd T 2 nd T + 1
224 fnimapr 2 nd 1 st T Fn 1 N 2 nd T 1 N 2 nd T + 1 1 N 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
225 68 19 23 224 syl3anc φ 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1
226 225 188 eqtrdi φ 2 nd 1 st T 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
227 222 223 226 3eqtr3d φ 2 nd 1 st U 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
228 227 f1oeq3d φ 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
229 195 228 mpbid φ 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
230 ssabral 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
231 f1oeq1 f = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
232 f1oeq1 f = 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
233 f1oeq1 f = 2 nd 1 st U 2 nd T 2 nd T + 1 f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
234 144 145 146 231 232 233 raltp f 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
235 230 234 bitri 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st U 2 nd T 2 nd T + 1 : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
236 182 191 229 235 syl3anbrc φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
237 hashss f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
238 163 236 237 sylancr φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T
239 153 enref 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1
240 hashprg 2 nd 1 st T 2 nd T + 1 V 2 nd 1 st T 2 nd T V 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2
241 80 184 240 mp2an 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2
242 96 241 sylib φ 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2
243 hashprg 2 nd T V 2 nd T + 1 V 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 = 2
244 74 75 243 mp2an 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 = 2
245 91 244 sylib φ 2 nd T 2 nd T + 1 = 2
246 242 245 eqtr4d φ 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2 nd T 2 nd T + 1
247 hashen 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin 2 nd T 2 nd T + 1 Fin 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1
248 155 156 247 mp2an 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1
249 246 248 sylib φ 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1
250 hashfacen 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1
251 239 249 250 sylancr φ f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1
252 153 153 mapval 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 = f | f : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1
253 mapfi 2 nd T 2 nd T + 1 Fin 2 nd T 2 nd T + 1 Fin 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 Fin
254 156 156 253 mp2an 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 Fin
255 252 254 eqeltrri f | f : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 Fin
256 f1of f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 f : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1
257 256 ss2abi f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1
258 ssfi f | f : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 Fin f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 Fin
259 255 257 258 mp2an f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 Fin
260 hashen f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T Fin f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 Fin f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1
261 163 259 260 mp2an f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1
262 251 261 sylibr φ f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1
263 hashfac 2 nd T 2 nd T + 1 Fin f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1 !
264 156 263 ax-mp f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1 !
265 245 fveq2d φ 2 nd T 2 nd T + 1 ! = 2 !
266 fac2 2 ! = 2
267 265 266 eqtrdi φ 2 nd T 2 nd T + 1 ! = 2
268 264 267 syl5eq φ f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd T 2 nd T + 1 = 2
269 262 268 eqtrd φ f | f : 2 nd T 2 nd T + 1 1-1 onto 2 nd 1 st T 2 nd T + 1 2 nd 1 st T 2 nd T = 2
270 238 269 breqtrd φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2
271 breq1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 2 3 2
272 270 271 syl5ibcom φ 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd T 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T + 1 2 nd 1 st U 2 nd T 2 nd T + 1 = 3 3 2
273 151 272 syld φ 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 3 2
274 273 necon1bd φ ¬ 3 2 2 nd 1 st U 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T
275 46 274 mpi φ 2 nd 1 st U 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T
276 coires1 2 nd 1 st T I 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1
277 128 276 eqtr4di φ 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T I 1 N 2 nd T 2 nd T + 1
278 275 277 uneq12d φ 2 nd 1 st U 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T I 1 N 2 nd T 2 nd T + 1
279 41 278 eqtr3d φ 2 nd 1 st U = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T I 1 N 2 nd T 2 nd T + 1
280 coundi 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T I 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T 2 nd 1 st T I 1 N 2 nd T 2 nd T + 1
281 279 280 eqtr4di φ 2 nd 1 st U = 2 nd 1 st T 2 nd T 2 nd T + 1 2 nd T + 1 2 nd T I 1 N 2 nd T 2 nd T + 1