Theorem cardS ≪ | index | src | ≫ 

pub theorem cardS (a s: nat): $ ~a e. s -> card (a ; s) = suc (card s) $;
StepHypRefExpression
1 elneq2 
z = s -> (a e. z <-> a e. s)
2 1 noteqd 
z = s -> (~a e. z <-> ~a e. s)
3 inseq2 
z = s -> a ; z = a ; s
4 3 cardeqd 
z = s -> card (a ; z) = card (a ; s)
5 cardeq 
z = s -> card z = card s
6 5 suceqd 
z = s -> suc (card z) = suc (card s)
7 4, 6 eqeqd 
z = s -> (card (a ; z) = suc (card z) <-> card (a ; s) = suc (card s))
8 2, 7 imeqd 
z = s -> (~a e. z -> card (a ; z) = suc (card z) <-> ~a e. s -> card (a ; s) = suc (card s))
9 8 eale 
A. z (~a e. z -> card (a ; z) = suc (card z)) -> ~a e. s -> card (a ; s) = suc (card s)
10 eleq1 
x = a -> (x e. z <-> a e. z)
11 10 noteqd 
x = a -> (~x e. z <-> ~a e. z)
12 inseq1 
x = a -> x ; z = a ; z
13 12 cardeqd 
x = a -> card (x ; z) = card (a ; z)
14 13 eqeq1d 
x = a -> (card (x ; z) = suc (card z) <-> card (a ; z) = suc (card z))
15 11, 14 imeqd 
x = a -> (~x e. z -> card (x ; z) = suc (card z) <-> ~a e. z -> card (a ; z) = suc (card z))
16 15 aleqd 
x = a -> (A. z (~x e. z -> card (x ; z) = suc (card z)) <-> A. z (~a e. z -> card (a ; z) = suc (card z)))
17 eleq1 
x = y -> (x e. z <-> y e. z)
18 17 noteqd 
x = y -> (~x e. z <-> ~y e. z)
19 inseq1 
x = y -> x ; z = y ; z
20 19 cardeqd 
x = y -> card (x ; z) = card (y ; z)
21 20 eqeq1d 
x = y -> (card (x ; z) = suc (card z) <-> card (y ; z) = suc (card z))
22 18, 21 imeqd 
x = y -> (~x e. z -> card (x ; z) = suc (card z) <-> ~y e. z -> card (y ; z) = suc (card z))
23 22 aleqd 
x = y -> (A. z (~x e. z -> card (x ; z) = suc (card z)) <-> A. z (~y e. z -> card (y ; z) = suc (card z)))
24 elneq2 
z = w -> (y e. z <-> y e. w)
25 24 noteqd 
z = w -> (~y e. z <-> ~y e. w)
26 inseq2 
z = w -> y ; z = y ; w
27 26 cardeqd 
z = w -> card (y ; z) = card (y ; w)
28 cardeq 
z = w -> card z = card w
29 28 suceqd 
z = w -> suc (card z) = suc (card w)
30 27, 29 eqeqd 
z = w -> (card (y ; z) = suc (card z) <-> card (y ; w) = suc (card w))
31 25, 30 imeqd 
z = w -> (~y e. z -> card (y ; z) = suc (card z) <-> ~y e. w -> card (y ; w) = suc (card w))
32 31 cbval 
A. z (~y e. z -> card (y ; z) = suc (card z)) <-> A. w (~y e. w -> card (y ; w) = suc (card w))
33 noteq 
(0 e. w <-> odd w) -> (~0 e. w <-> ~odd w)
34 el01 
0 e. w <-> odd w
35 33, 34 ax_mp 
~0 e. w <-> ~odd w
36 eqb0 
~odd w <-> w = b0 (w // 2)
37 b1ins 
b1 (w // 2) = 0 ; b0 (w // 2)
38 inseq2 
w = b0 (w // 2) -> 0 ; w = 0 ; b0 (w // 2)
39 37, 38 syl6eqr 
w = b0 (w // 2) -> 0 ; w = b1 (w // 2)
40 39 cardeqd 
w = b0 (w // 2) -> card (0 ; w) = card (b1 (w // 2))
41 cardb1 
card (b1 (w // 2)) = suc (card (w // 2))
42 cardb0 
card (b0 (w // 2)) = card (w // 2)
43 cardeq 
w = b0 (w // 2) -> card w = card (b0 (w // 2))
44 42, 43 syl6eq 
w = b0 (w // 2) -> card w = card (w // 2)
45 44 suceqd 
w = b0 (w // 2) -> suc (card w) = suc (card (w // 2))
46 41, 45 syl6eqr 
w = b0 (w // 2) -> suc (card w) = card (b1 (w // 2))
47 40, 46 eqtr4d 
w = b0 (w // 2) -> card (0 ; w) = suc (card w)
48 36, 47 sylbi 
~odd w -> card (0 ; w) = suc (card w)
49 35, 48 sylbi 
~0 e. w -> card (0 ; w) = suc (card w)
50 eleq1 
y = 0 -> (y e. w <-> 0 e. w)
51 50 noteqd 
y = 0 -> (~y e. w <-> ~0 e. w)
52 inseq1 
y = 0 -> y ; w = 0 ; w
53 52 cardeqd 
y = 0 -> card (y ; w) = card (0 ; w)
54 53 eqeq1d 
y = 0 -> (card (y ; w) = suc (card w) <-> card (0 ; w) = suc (card w))
55 51, 54 imeqd 
y = 0 -> (~y e. w -> card (y ; w) = suc (card w) <-> ~0 e. w -> card (0 ; w) = suc (card w))
56 49, 55 mpbiri 
y = 0 -> ~y e. w -> card (y ; w) = suc (card w)
57 56 a1d 
y = 0 -> A. x (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> ~y e. w -> card (y ; w) = suc (card w)
58 biim1 
x < y -> (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z)) <-> A. z (~x e. z -> card (x ; z) = suc (card z)))
59 anr 
~y = 0 /\ x = y - 1 -> x = y - 1
60 59 lteq1d 
~y = 0 /\ x = y - 1 -> (x < y <-> y - 1 < y)
61 subltid 
0 < y /\ 0 < 1 -> y - 1 < y
62 lt01 
0 < y <-> y != 0
63 anl 
~y = 0 /\ x = y - 1 -> ~y = 0
64 63 conv ne 
~y = 0 /\ x = y - 1 -> y != 0
65 62, 64 sylibr 
~y = 0 /\ x = y - 1 -> 0 < y
66 d0lt1 
0 < 1
67 66 a1i 
~y = 0 /\ x = y - 1 -> 0 < 1
68 61, 65, 67 sylan 
~y = 0 /\ x = y - 1 -> y - 1 < y
69 60, 68 mpbird 
~y = 0 /\ x = y - 1 -> x < y
70 58, 69 syl 
~y = 0 /\ x = y - 1 -> (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z)) <-> A. z (~x e. z -> card (x ; z) = suc (card z)))
71 70 imeq1d 
~y = 0 /\ x = y - 1 ->
  ((x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> ~y e. w -> card (y ; w) = suc (card w) <->
    A. z (~x e. z -> card (x ; z) = suc (card z)) -> ~y e. w -> card (y ; w) = suc (card w))
72 anlr 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> x = y - 1
73 anr 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> z = w // 2
74 72, 73 elneqd 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> (x e. z <-> y - 1 e. w // 2)
75 eldiv2 
y - 1 e. w // 2 <-> suc (y - 1) e. w
76 sub1can 
y != 0 -> suc (y - 1) = y
77 anll 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> ~y = 0
78 77 conv ne 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> y != 0
79 76, 78 syl 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> suc (y - 1) = y
80 79 eleq1d 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> (suc (y - 1) e. w <-> y e. w)
81 75, 80 syl5bb 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> (y - 1 e. w // 2 <-> y e. w)
82 74, 81 bitrd 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> (x e. z <-> y e. w)
83 82 noteqd 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> (~x e. z <-> ~y e. w)
84 83 bi2d 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> ~y e. w -> ~x e. z
85 anass 
~y = 0 /\ x = y - 1 /\ z = w // 2 <-> ~y = 0 /\ (x = y - 1 /\ z = w // 2)
86 insdiv2 
suc (y - 1) ; w // 2 = (y - 1) ; (w // 2)
87 inseq 
x = y - 1 -> z = w // 2 -> x ; z = (y - 1) ; (w // 2)
88 87 imp 
x = y - 1 /\ z = w // 2 -> x ; z = (y - 1) ; (w // 2)
89 86, 88 syl6eqr 
x = y - 1 /\ z = w // 2 -> x ; z = suc (y - 1) ; w // 2
90 89 cardeqd 
x = y - 1 /\ z = w // 2 -> card (x ; z) = card (suc (y - 1) ; w // 2)
91 anr 
x = y - 1 /\ z = w // 2 -> z = w // 2
92 91 cardeqd 
x = y - 1 /\ z = w // 2 -> card z = card (w // 2)
93 92 suceqd 
x = y - 1 /\ z = w // 2 -> suc (card z) = suc (card (w // 2))
94 90, 93 eqeqd 
x = y - 1 /\ z = w // 2 -> (card (x ; z) = suc (card z) <-> card (suc (y - 1) ; w // 2) = suc (card (w // 2)))
95 94 imeq1d 
x = y - 1 /\ z = w // 2 ->
  (card (x ; z) = suc (card z) -> card (y ; w) = suc (card w) <-> card (suc (y - 1) ; w // 2) = suc (card (w // 2)) -> card (y ; w) = suc (card w))
96 peano2 
suc (card (suc (y - 1) ; w // 2)) = suc (suc (card (w // 2))) <-> card (suc (y - 1) ; w // 2) = suc (card (w // 2))
97 cardb1 
card (b1 (suc (y - 1) ; w // 2)) = suc (card (suc (y - 1) ; w // 2))
98 76 conv ne 
~y = 0 -> suc (y - 1) = y
99 98 anwl 
~y = 0 /\ odd w -> suc (y - 1) = y
100 99 inseq1d 
~y = 0 /\ odd w -> suc (y - 1) ; w = y ; w
101 100 diveq1d 
~y = 0 /\ odd w -> suc (y - 1) ; w // 2 = y ; w // 2
102 101 b1eqd 
~y = 0 /\ odd w -> b1 (suc (y - 1) ; w // 2) = b1 (y ; w // 2)
103 eqb1 
odd (y ; w) <-> y ; w = b1 (y ; w // 2)
104 el01 
0 e. y ; w <-> odd (y ; w)
105 elins 
0 e. y ; w <-> 0 = y \/ 0 e. w
106 anr 
~y = 0 /\ odd w -> odd w
107 34, 106 sylibr 
~y = 0 /\ odd w -> 0 e. w
108 107 orrd 
~y = 0 /\ odd w -> 0 = y \/ 0 e. w
109 105, 108 sylibr 
~y = 0 /\ odd w -> 0 e. y ; w
110 104, 109 sylib 
~y = 0 /\ odd w -> odd (y ; w)
111 103, 110 sylib 
~y = 0 /\ odd w -> y ; w = b1 (y ; w // 2)
112 102, 111 eqtr4d 
~y = 0 /\ odd w -> b1 (suc (y - 1) ; w // 2) = y ; w
113 112 cardeqd 
~y = 0 /\ odd w -> card (b1 (suc (y - 1) ; w // 2)) = card (y ; w)
114 97, 113 syl5eqr 
~y = 0 /\ odd w -> suc (card (suc (y - 1) ; w // 2)) = card (y ; w)
115 eqb1 
odd w <-> w = b1 (w // 2)
116 115, 106 sylib 
~y = 0 /\ odd w -> w = b1 (w // 2)
117 116 eqcomd 
~y = 0 /\ odd w -> b1 (w // 2) = w
118 117 cardeqd 
~y = 0 /\ odd w -> card (b1 (w // 2)) = card w
119 41, 118 syl5eqr 
~y = 0 /\ odd w -> suc (card (w // 2)) = card w
120 119 suceqd 
~y = 0 /\ odd w -> suc (suc (card (w // 2))) = suc (card w)
121 114, 120 eqeqd 
~y = 0 /\ odd w -> (suc (card (suc (y - 1) ; w // 2)) = suc (suc (card (w // 2))) <-> card (y ; w) = suc (card w))
122 96, 121 syl5bbr 
~y = 0 /\ odd w -> (card (suc (y - 1) ; w // 2) = suc (card (w // 2)) <-> card (y ; w) = suc (card w))
123 cardb0 
card (b0 (suc (y - 1) ; w // 2)) = card (suc (y - 1) ; w // 2)
124 98 anwl 
~y = 0 /\ ~odd w -> suc (y - 1) = y
125 124 inseq1d 
~y = 0 /\ ~odd w -> suc (y - 1) ; w = y ; w
126 125 diveq1d 
~y = 0 /\ ~odd w -> suc (y - 1) ; w // 2 = y ; w // 2
127 126 b0eqd 
~y = 0 /\ ~odd w -> b0 (suc (y - 1) ; w // 2) = b0 (y ; w // 2)
128 eqb0 
~odd (y ; w) <-> y ; w = b0 (y ; w // 2)
129 notor 
~(y = 0 \/ odd w) <-> ~y = 0 /\ ~odd w
130 con3 
(odd (y ; w) -> y = 0 \/ odd w) -> ~(y = 0 \/ odd w) -> ~odd (y ; w)
131 bi1 
(0 = y \/ 0 e. w <-> y = 0 \/ odd w) -> 0 = y \/ 0 e. w -> y = 0 \/ odd w
132 oreq 
(0 = y <-> y = 0) -> (0 e. w <-> odd w) -> (0 = y \/ 0 e. w <-> y = 0 \/ odd w)
133 eqcomb 
0 = y <-> y = 0
134 132, 133 ax_mp 
(0 e. w <-> odd w) -> (0 = y \/ 0 e. w <-> y = 0 \/ odd w)
135 134, 34 ax_mp 
0 = y \/ 0 e. w <-> y = 0 \/ odd w
136 131, 135 ax_mp 
0 = y \/ 0 e. w -> y = 0 \/ odd w
137 105, 136 sylbi 
0 e. y ; w -> y = 0 \/ odd w
138 104, 137 sylbir 
odd (y ; w) -> y = 0 \/ odd w
139 130, 138 ax_mp 
~(y = 0 \/ odd w) -> ~odd (y ; w)
140 129, 139 sylbir 
~y = 0 /\ ~odd w -> ~odd (y ; w)
141 128, 140 sylib 
~y = 0 /\ ~odd w -> y ; w = b0 (y ; w // 2)
142 127, 141 eqtr4d 
~y = 0 /\ ~odd w -> b0 (suc (y - 1) ; w // 2) = y ; w
143 142 cardeqd 
~y = 0 /\ ~odd w -> card (b0 (suc (y - 1) ; w // 2)) = card (y ; w)
144 123, 143 syl5eqr 
~y = 0 /\ ~odd w -> card (suc (y - 1) ; w // 2) = card (y ; w)
145 anr 
~y = 0 /\ ~odd w -> ~odd w
146 36, 145 sylib 
~y = 0 /\ ~odd w -> w = b0 (w // 2)
147 146 eqcomd 
~y = 0 /\ ~odd w -> b0 (w // 2) = w
148 147 cardeqd 
~y = 0 /\ ~odd w -> card (b0 (w // 2)) = card w
149 42, 148 syl5eqr 
~y = 0 /\ ~odd w -> card (w // 2) = card w
150 149 suceqd 
~y = 0 /\ ~odd w -> suc (card (w // 2)) = suc (card w)
151 144, 150 eqeqd 
~y = 0 /\ ~odd w -> (card (suc (y - 1) ; w // 2) = suc (card (w // 2)) <-> card (y ; w) = suc (card w))
152 122, 151 casesda 
~y = 0 -> (card (suc (y - 1) ; w // 2) = suc (card (w // 2)) <-> card (y ; w) = suc (card w))
153 152 bi1d 
~y = 0 -> card (suc (y - 1) ; w // 2) = suc (card (w // 2)) -> card (y ; w) = suc (card w)
154 95, 153 syl5ibrcom 
~y = 0 -> x = y - 1 /\ z = w // 2 -> card (x ; z) = suc (card z) -> card (y ; w) = suc (card w)
155 154 imp 
~y = 0 /\ (x = y - 1 /\ z = w // 2) -> card (x ; z) = suc (card z) -> card (y ; w) = suc (card w)
156 85, 155 sylbi 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> card (x ; z) = suc (card z) -> card (y ; w) = suc (card w)
157 84, 156 imimd 
~y = 0 /\ x = y - 1 /\ z = w // 2 -> (~x e. z -> card (x ; z) = suc (card z)) -> ~y e. w -> card (y ; w) = suc (card w)
158 157 ealde 
~y = 0 /\ x = y - 1 -> A. z (~x e. z -> card (x ; z) = suc (card z)) -> ~y e. w -> card (y ; w) = suc (card w)
159 71, 158 mpbird 
~y = 0 /\ x = y - 1 -> (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> ~y e. w -> card (y ; w) = suc (card w)
160 159 ealde 
~y = 0 -> A. x (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> ~y e. w -> card (y ; w) = suc (card w)
161 57, 160 cases 
A. x (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> ~y e. w -> card (y ; w) = suc (card w)
162 161 iald 
A. x (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> A. w (~y e. w -> card (y ; w) = suc (card w))
163 32, 162 sylibr 
A. x (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> A. z (~y e. z -> card (y ; z) = suc (card z))
164 163 anwr 
T. /\ A. x (x < y -> A. z (~x e. z -> card (x ; z) = suc (card z))) -> A. z (~y e. z -> card (y ; z) = suc (card z))
165 16, 23, 164 indstr 
T. -> A. z (~a e. z -> card (a ; z) = suc (card z))
166 165 trud 
A. z (~a e. z -> card (a ; z) = suc (card z))
167 9, 166 ax_mp 
~a e. s -> card (a ; s) = suc (card s)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)