Theorem nnsucelr 4429

Description: Transfer membership in the successor of a natural into membership of the natural itself. Theorem X.1.17 of [Rosser] p. 525. (Contributed by SF, 14-Jan-2015.)

Hypotheses

Ref	Expression
nnsucelr.1	|- A e. _V
nnsucelr.2	|- X e. _V

Assertion

Ref	Expression
nnsucelr	|- ((M e. Nn /\ (-. X e. A /\ (A u. {X}) e. (M +o 1c))) -> A e. M)

Proof of Theorem nnsucelr

Dummy variables a c m n x y z b d w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnsucelrlem1 4425	. . . 4 |- {m | A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m)} e. _V
2		addceq1 4384	. . . . . . . . . 10 |- (m = 0c -> (m +o 1c) = (0c +o 1c))
3		addcid2 4408	. . . . . . . . . 10 |- (0c +o 1c) = 1c
4	2, 3	syl6eq 2401	. . . . . . . . 9 |- (m = 0c -> (m +o 1c) = 1c)
5	4	eleq2d 2420	. . . . . . . 8 |- (m = 0c -> ((a u. {x}) e. (m +o 1c) <-> (a u. {x}) e. 1c))
6		el1c 4140	. . . . . . . 8 |- ((a u. {x}) e. 1c <-> E.y(a u. {x}) = {y})
7	5, 6	syl6bb 252	. . . . . . 7 |- (m = 0c -> ((a u. {x}) e. (m +o 1c) <-> E.y(a u. {x}) = {y}))
8	7	anbi2d 684	. . . . . 6 |- (m = 0c -> ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) <-> (-. x e. a /\ E.y(a u. {x}) = {y})))
9		eleq2 2414	. . . . . . 7 |- (m = 0c -> (a e. m <-> a e. 0c))
10		df-0c 4378	. . . . . . . . 9 |- 0c = {(/)}
11	10	eleq2i 2417	. . . . . . . 8 |- (a e. 0c <-> a e. {(/)})
12		vex 2863	. . . . . . . . 9 |- a e. _V
13	12	elsnc 3757	. . . . . . . 8 |- (a e. {(/)} <-> a = (/))
14	11, 13	bitri 240	. . . . . . 7 |- (a e. 0c <-> a = (/))
15	9, 14	syl6bb 252	. . . . . 6 |- (m = 0c -> (a e. m <-> a = (/)))
16	8, 15	imbi12d 311	. . . . 5 |- (m = 0c -> (((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> ((-. x e. a /\ E.y(a u. {x}) = {y}) -> a = (/))))
17	16	2albidv 1627	. . . 4 |- (m = 0c -> (A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> A.aA.x((-. x e. a /\ E.y(a u. {x}) = {y}) -> a = (/))))
18		addceq1 4384	. . . . . . . . 9 |- (m = n -> (m +o 1c) = (n +o 1c))
19	18	eleq2d 2420	. . . . . . . 8 |- (m = n -> ((a u. {x}) e. (m +o 1c) <-> (a u. {x}) e. (n +o 1c)))
20	19	anbi2d 684	. . . . . . 7 |- (m = n -> ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) <-> (-. x e. a /\ (a u. {x}) e. (n +o 1c))))
21		eleq2 2414	. . . . . . 7 |- (m = n -> (a e. m <-> a e. n))
22	20, 21	imbi12d 311	. . . . . 6 |- (m = n -> (((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> ((-. x e. a /\ (a u. {x}) e. (n +o 1c)) -> a e. n)))
23	22	2albidv 1627	. . . . 5 |- (m = n -> (A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> A.aA.x((-. x e. a /\ (a u. {x}) e. (n +o 1c)) -> a e. n)))
24		eleq12 2415	. . . . . . . . . 10 |- ((x = z /\ a = c) -> (x e. a <-> z e. c))
25	24	ancoms 439	. . . . . . . . 9 |- ((a = c /\ x = z) -> (x e. a <-> z e. c))
26	25	notbid 285	. . . . . . . 8 |- ((a = c /\ x = z) -> (-. x e. a <-> -. z e. c))
27		sneq 3745	. . . . . . . . . 10 |- (x = z -> {x} = {z})
28		uneq12 3414	. . . . . . . . . 10 |- ((a = c /\ {x} = {z}) -> (a u. {x}) = (c u. {z}))
29	27, 28	sylan2 460	. . . . . . . . 9 |- ((a = c /\ x = z) -> (a u. {x}) = (c u. {z}))
30	29	eleq1d 2419	. . . . . . . 8 |- ((a = c /\ x = z) -> ((a u. {x}) e. (n +o 1c) <-> (c u. {z}) e. (n +o 1c)))
31	26, 30	anbi12d 691	. . . . . . 7 |- ((a = c /\ x = z) -> ((-. x e. a /\ (a u. {x}) e. (n +o 1c)) <-> (-. z e. c /\ (c u. {z}) e. (n +o 1c))))
32		eleq1 2413	. . . . . . . 8 |- (a = c -> (a e. n <-> c e. n))
33	32	adantr 451	. . . . . . 7 |- ((a = c /\ x = z) -> (a e. n <-> c e. n))
34	31, 33	imbi12d 311	. . . . . 6 |- ((a = c /\ x = z) -> (((-. x e. a /\ (a u. {x}) e. (n +o 1c)) -> a e. n) <-> ((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n)))
35	34	cbval2v 2006	. . . . 5 |- (A.aA.x((-. x e. a /\ (a u. {x}) e. (n +o 1c)) -> a e. n) <-> A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n))
36	23, 35	syl6bb 252	. . . 4 |- (m = n -> (A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n)))
37		addceq1 4384	. . . . . . . 8 |- (m = (n +o 1c) -> (m +o 1c) = ((n +o 1c) +o 1c))
38	37	eleq2d 2420	. . . . . . 7 |- (m = (n +o 1c) -> ((a u. {x}) e. (m +o 1c) <-> (a u. {x}) e. ((n +o 1c) +o 1c)))
39	38	anbi2d 684	. . . . . 6 |- (m = (n +o 1c) -> ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) <-> (-. x e. a /\ (a u. {x}) e. ((n +o 1c) +o 1c))))
40		eleq2 2414	. . . . . 6 |- (m = (n +o 1c) -> (a e. m <-> a e. (n +o 1c)))
41	39, 40	imbi12d 311	. . . . 5 |- (m = (n +o 1c) -> (((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> ((-. x e. a /\ (a u. {x}) e. ((n +o 1c) +o 1c)) -> a e. (n +o 1c))))
42	41	2albidv 1627	. . . 4 |- (m = (n +o 1c) -> (A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> A.aA.x((-. x e. a /\ (a u. {x}) e. ((n +o 1c) +o 1c)) -> a e. (n +o 1c))))
43		addceq1 4384	. . . . . . . 8 |- (m = M -> (m +o 1c) = (M +o 1c))
44	43	eleq2d 2420	. . . . . . 7 |- (m = M -> ((a u. {x}) e. (m +o 1c) <-> (a u. {x}) e. (M +o 1c)))
45	44	anbi2d 684	. . . . . 6 |- (m = M -> ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) <-> (-. x e. a /\ (a u. {x}) e. (M +o 1c))))
46		eleq2 2414	. . . . . 6 |- (m = M -> (a e. m <-> a e. M))
47	45, 46	imbi12d 311	. . . . 5 |- (m = M -> (((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> ((-. x e. a /\ (a u. {x}) e. (M +o 1c)) -> a e. M)))
48	47	2albidv 1627	. . . 4 |- (m = M -> (A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> A.aA.x((-. x e. a /\ (a u. {x}) e. (M +o 1c)) -> a e. M)))
49		vex 2863	. . . . . . . . . . 11 |- x e. _V
50	49	unsneqsn 3888	. . . . . . . . . 10 |- ((a u. {x}) = {y} -> (a = (/) \/ a = {x}))
51	50	ord 366	. . . . . . . . 9 |- ((a u. {x}) = {y} -> (-. a = (/) -> a = {x}))
52	49	snid 3761	. . . . . . . . . 10 |- x e. {x}
53		eleq2 2414	. . . . . . . . . 10 |- (a = {x} -> (x e. a <-> x e. {x}))
54	52, 53	mpbiri 224	. . . . . . . . 9 |- (a = {x} -> x e. a)
55	51, 54	syl6 29	. . . . . . . 8 |- ((a u. {x}) = {y} -> (-. a = (/) -> x e. a))
56	55	con1d 116	. . . . . . 7 |- ((a u. {x}) = {y} -> (-. x e. a -> a = (/)))
57	56	exlimiv 1634	. . . . . 6 |- (E.y(a u. {x}) = {y} -> (-. x e. a -> a = (/)))
58	57	impcom 419	. . . . 5 |- ((-. x e. a /\ E.y(a u. {x}) = {y}) -> a = (/))
59	58	gen2 1547	. . . 4 |- A.aA.x((-. x e. a /\ E.y(a u. {x}) = {y}) -> a = (/))
60		elsuc 4414	. . . . . . . . 9 |- ((a u. {x}) e. ((n +o 1c) +o 1c) <-> E.b e. (n +o 1c)E.y e. ∼ b(a u. {x}) = (b u. {y}))
61		vex 2863	. . . . . . . . . . . . 13 |- y e. _V
62	61	elcompl 3226	. . . . . . . . . . . 12 |- (y e. ∼ b <-> -. y e. b)
63	62	anbi2i 675	. . . . . . . . . . 11 |- ((b e. (n +o 1c) /\ y e. ∼ b) <-> (b e. (n +o 1c) /\ -. y e. b))
64		simprrl 740	. . . . . . . . . . . . . . . . . . 19 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> (a u. {x}) = (b u. {y}))
65		sneq 3745	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> {x} = {y})
66	65	adantr 451	. . . . . . . . . . . . . . . . . . 19 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> {x} = {y})
67	64, 66	difeq12d 3387	. . . . . . . . . . . . . . . . . 18 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> ((a u. {x}) \ {x}) = ((b u. {y}) \ {y}))
68		simprrr 741	. . . . . . . . . . . . . . . . . . 19 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> -. x e. a)
69		nnsucelrlem2 4426	. . . . . . . . . . . . . . . . . . 19 |- (-. x e. a -> ((a u. {x}) \ {x}) = a)
70	68, 69	syl 15	. . . . . . . . . . . . . . . . . 18 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> ((a u. {x}) \ {x}) = a)
71		simprlr 739	. . . . . . . . . . . . . . . . . . 19 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> -. y e. b)
72		nnsucelrlem2 4426	. . . . . . . . . . . . . . . . . . 19 |- (-. y e. b -> ((b u. {y}) \ {y}) = b)
73	71, 72	syl 15	. . . . . . . . . . . . . . . . . 18 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> ((b u. {y}) \ {y}) = b)
74	67, 70, 73	3eqtr3d 2393	. . . . . . . . . . . . . . . . 17 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> a = b)
75		simprll 738	. . . . . . . . . . . . . . . . 17 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> b e. (n +o 1c))
76	74, 75	eqeltrd 2427	. . . . . . . . . . . . . . . 16 |- ((x = y /\ ((b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> a e. (n +o 1c))
77	76	3adantr1 1114	. . . . . . . . . . . . . . 15 |- ((x = y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> a e. (n +o 1c))
78	77	ex 423	. . . . . . . . . . . . . 14 |- (x = y -> ((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) -> a e. (n +o 1c)))
79		simpl 443	. . . . . . . . . . . . . . . . 17 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> x =/= y)
80		simpr3l 1016	. . . . . . . . . . . . . . . . 17 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> (a u. {x}) = (b u. {y}))
81		simpr2r 1015	. . . . . . . . . . . . . . . . 17 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> -. y e. b)
82	49	nnsucelrlem3 4427	. . . . . . . . . . . . . . . . 17 |- ((x =/= y /\ (a u. {x}) = (b u. {y}) /\ -. y e. b) -> b = ((a \ {y}) u. {x}))
83	79, 80, 81, 82	syl3anc 1182	. . . . . . . . . . . . . . . 16 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> b = ((a \ {y}) u. {x}))
84		simp22r 1075	. . . . . . . . . . . . . . . . . . 19 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> -. y e. b)
85		difsn 3846	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (-. y e. a -> (a \ {y}) = a)
86	85	uneq1d 3418	. . . . . . . . . . . . . . . . . . . . . . 23 |- (-. y e. a -> ((a \ {y}) u. {x}) = (a u. {x}))
87	86	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . . . 22 |- (-. y e. a -> (b = ((a \ {y}) u. {x}) <-> b = (a u. {x})))
88	87	biimpcd 215	. . . . . . . . . . . . . . . . . . . . 21 |- (b = ((a \ {y}) u. {x}) -> (-. y e. a -> b = (a u. {x})))
89	88	3ad2ant3 978	. . . . . . . . . . . . . . . . . . . 20 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (-. y e. a -> b = (a u. {x})))
90		simp23l 1076	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (a u. {x}) = (b u. {y}))
91	90	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . . 21 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (b = (a u. {x}) <-> b = (b u. {y})))
92	61	snss 3839	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. b <-> {y} C_ b)
93		ssequn2 3437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({y} C_ b <-> (b u. {y}) = b)
94	92, 93	bitr2i 241	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((b u. {y}) = b <-> y e. b)
95	94	biimpi 186	. . . . . . . . . . . . . . . . . . . . . 22 |- ((b u. {y}) = b -> y e. b)
96	95	eqcoms 2356	. . . . . . . . . . . . . . . . . . . . 21 |- (b = (b u. {y}) -> y e. b)
97	91, 96	syl6bi 219	. . . . . . . . . . . . . . . . . . . 20 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (b = (a u. {x}) -> y e. b))
98	89, 97	syld 40	. . . . . . . . . . . . . . . . . . 19 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (-. y e. a -> y e. b))
99	84, 98	mt3d 117	. . . . . . . . . . . . . . . . . 18 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> y e. a)
100		nnsucelrlem4 4428	. . . . . . . . . . . . . . . . . 18 |- (y e. a -> ((a \ {y}) u. {y}) = a)
101	99, 100	syl 15	. . . . . . . . . . . . . . . . 17 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> ((a \ {y}) u. {y}) = a)
102		simpl3r 1011	. . . . . . . . . . . . . . . . . . . . 21 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> -. x e. a)
103		difss 3394	. . . . . . . . . . . . . . . . . . . . . 22 |- (a \ {y}) C_ a
104	103	sseli 3270	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. (a \ {y}) -> x e. a)
105	102, 104	nsyl 113	. . . . . . . . . . . . . . . . . . . 20 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> -. x e. (a \ {y}))
106		simp2l 981	. . . . . . . . . . . . . . . . . . . . 21 |- ((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) -> b e. (n +o 1c))
107		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . 22 |- (b = ((a \ {y}) u. {x}) -> (b e. (n +o 1c) <-> ((a \ {y}) u. {x}) e. (n +o 1c)))
108	107	biimpd 198	. . . . . . . . . . . . . . . . . . . . 21 |- (b = ((a \ {y}) u. {x}) -> (b e. (n +o 1c) -> ((a \ {y}) u. {x}) e. (n +o 1c)))
109	106, 108	mpan9 455	. . . . . . . . . . . . . . . . . . . 20 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> ((a \ {y}) u. {x}) e. (n +o 1c))
110		simpl1 958	. . . . . . . . . . . . . . . . . . . . 21 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n))
111		snex 4112	. . . . . . . . . . . . . . . . . . . . . . 23 |- {y} e. _V
112	12, 111	difex 4108	. . . . . . . . . . . . . . . . . . . . . 22 |- (a \ {y}) e. _V
113		eleq12 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z = x /\ c = (a \ {y})) -> (z e. c <-> x e. (a \ {y})))
114	113	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c = (a \ {y}) /\ z = x) -> (z e. c <-> x e. (a \ {y})))
115	114	notbid 285	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((c = (a \ {y}) /\ z = x) -> (-. z e. c <-> -. x e. (a \ {y})))
116		sneq 3745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z = x -> {z} = {x})
117		uneq12 3414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c = (a \ {y}) /\ {z} = {x}) -> (c u. {z}) = ((a \ {y}) u. {x}))
118	116, 117	sylan2 460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c = (a \ {y}) /\ z = x) -> (c u. {z}) = ((a \ {y}) u. {x}))
119	118	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((c = (a \ {y}) /\ z = x) -> ((c u. {z}) e. (n +o 1c) <-> ((a \ {y}) u. {x}) e. (n +o 1c)))
120	115, 119	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((c = (a \ {y}) /\ z = x) -> ((-. z e. c /\ (c u. {z}) e. (n +o 1c)) <-> (-. x e. (a \ {y}) /\ ((a \ {y}) u. {x}) e. (n +o 1c))))
121		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c = (a \ {y}) -> (c e. n <-> (a \ {y}) e. n))
122	121	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((c = (a \ {y}) /\ z = x) -> (c e. n <-> (a \ {y}) e. n))
123	120, 122	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((c = (a \ {y}) /\ z = x) -> (((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) <-> ((-. x e. (a \ {y}) /\ ((a \ {y}) u. {x}) e. (n +o 1c)) -> (a \ {y}) e. n)))
124	123	spc2gv 2943	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a \ {y}) e. _V /\ x e. _V) -> (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> ((-. x e. (a \ {y}) /\ ((a \ {y}) u. {x}) e. (n +o 1c)) -> (a \ {y}) e. n)))
125	112, 49, 124	mp2an 653	. . . . . . . . . . . . . . . . . . . . 21 |- (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> ((-. x e. (a \ {y}) /\ ((a \ {y}) u. {x}) e. (n +o 1c)) -> (a \ {y}) e. n))
126	110, 125	syl 15	. . . . . . . . . . . . . . . . . . . 20 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> ((-. x e. (a \ {y}) /\ ((a \ {y}) u. {x}) e. (n +o 1c)) -> (a \ {y}) e. n))
127	105, 109, 126	mp2and 660	. . . . . . . . . . . . . . . . . . 19 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (a \ {y}) e. n)
128	127	3adant1 973	. . . . . . . . . . . . . . . . . 18 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> (a \ {y}) e. n)
129	61	snid 3761	. . . . . . . . . . . . . . . . . . . . 21 |- y e. {y}
130		eldif 3222	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. (a \ {y}) <-> (y e. a /\ -. y e. {y}))
131	130	simprbi 450	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. (a \ {y}) -> -. y e. {y})
132	129, 131	mt2 170	. . . . . . . . . . . . . . . . . . . 20 |- -. y e. (a \ {y})
133	61	elcompl 3226	. . . . . . . . . . . . . . . . . . . 20 |- (y e. ∼ (a \ {y}) <-> -. y e. (a \ {y}))
134	132, 133	mpbir 200	. . . . . . . . . . . . . . . . . . 19 |- y e. ∼ (a \ {y})
135		eqid 2353	. . . . . . . . . . . . . . . . . . 19 |- ((a \ {y}) u. {y}) = ((a \ {y}) u. {y})
136		sneq 3745	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = y -> {w} = {y})
137	136	uneq2d 3419	. . . . . . . . . . . . . . . . . . . . 21 |- (w = y -> ((a \ {y}) u. {w}) = ((a \ {y}) u. {y}))
138	137	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . 20 |- (w = y -> (((a \ {y}) u. {y}) = ((a \ {y}) u. {w}) <-> ((a \ {y}) u. {y}) = ((a \ {y}) u. {y})))
139	138	rspcev 2956	. . . . . . . . . . . . . . . . . . 19 |- ((y e. ∼ (a \ {y}) /\ ((a \ {y}) u. {y}) = ((a \ {y}) u. {y})) -> E.w e. ∼ (a \ {y})((a \ {y}) u. {y}) = ((a \ {y}) u. {w}))
140	134, 135, 139	mp2an 653	. . . . . . . . . . . . . . . . . 18 |- E.w e. ∼ (a \ {y})((a \ {y}) u. {y}) = ((a \ {y}) u. {w})
141		compleq 3244	. . . . . . . . . . . . . . . . . . . . 21 |- (d = (a \ {y}) -> ∼ d = ∼ (a \ {y}))
142		uneq1 3412	. . . . . . . . . . . . . . . . . . . . . 22 |- (d = (a \ {y}) -> (d u. {w}) = ((a \ {y}) u. {w}))
143	142	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . . 21 |- (d = (a \ {y}) -> (((a \ {y}) u. {y}) = (d u. {w}) <-> ((a \ {y}) u. {y}) = ((a \ {y}) u. {w})))
144	141, 143	rexeqbidv 2821	. . . . . . . . . . . . . . . . . . . 20 |- (d = (a \ {y}) -> (E.w e. ∼ d((a \ {y}) u. {y}) = (d u. {w}) <-> E.w e. ∼ (a \ {y})((a \ {y}) u. {y}) = ((a \ {y}) u. {w})))
145	144	rspcev 2956	. . . . . . . . . . . . . . . . . . 19 |- (((a \ {y}) e. n /\ E.w e. ∼ (a \ {y})((a \ {y}) u. {y}) = ((a \ {y}) u. {w})) -> E.d e. n E.w e. ∼ d((a \ {y}) u. {y}) = (d u. {w}))
146		elsuc 4414	. . . . . . . . . . . . . . . . . . 19 |- (((a \ {y}) u. {y}) e. (n +o 1c) <-> E.d e. n E.w e. ∼ d((a \ {y}) u. {y}) = (d u. {w}))
147	145, 146	sylibr 203	. . . . . . . . . . . . . . . . . 18 |- (((a \ {y}) e. n /\ E.w e. ∼ (a \ {y})((a \ {y}) u. {y}) = ((a \ {y}) u. {w})) -> ((a \ {y}) u. {y}) e. (n +o 1c))
148	128, 140, 147	sylancl 643	. . . . . . . . . . . . . . . . 17 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> ((a \ {y}) u. {y}) e. (n +o 1c))
149	101, 148	eqeltrrd 2428	. . . . . . . . . . . . . . . 16 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) /\ b = ((a \ {y}) u. {x})) -> a e. (n +o 1c))
150	83, 149	mpd3an3 1278	. . . . . . . . . . . . . . 15 |- ((x =/= y /\ (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a))) -> a e. (n +o 1c))
151	150	ex 423	. . . . . . . . . . . . . 14 |- (x =/= y -> ((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) -> a e. (n +o 1c)))
152	78, 151	pm2.61ine 2593	. . . . . . . . . . . . 13 |- ((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) -> a e. (n +o 1c))
153	152	3expa 1151	. . . . . . . . . . . 12 |- (((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b)) /\ ((a u. {x}) = (b u. {y}) /\ -. x e. a)) -> a e. (n +o 1c))
154	153	exp32 588	. . . . . . . . . . 11 |- ((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ -. y e. b)) -> ((a u. {x}) = (b u. {y}) -> (-. x e. a -> a e. (n +o 1c))))
155	63, 154	sylan2b 461	. . . . . . . . . 10 |- ((A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) /\ (b e. (n +o 1c) /\ y e. ∼ b)) -> ((a u. {x}) = (b u. {y}) -> (-. x e. a -> a e. (n +o 1c))))
156	155	rexlimdvva 2746	. . . . . . . . 9 |- (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> (E.b e. (n +o 1c)E.y e. ∼ b(a u. {x}) = (b u. {y}) -> (-. x e. a -> a e. (n +o 1c))))
157	60, 156	syl5bi 208	. . . . . . . 8 |- (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> ((a u. {x}) e. ((n +o 1c) +o 1c) -> (-. x e. a -> a e. (n +o 1c))))
158	157	com23 72	. . . . . . 7 |- (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> (-. x e. a -> ((a u. {x}) e. ((n +o 1c) +o 1c) -> a e. (n +o 1c))))
159	158	imp3a 420	. . . . . 6 |- (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> ((-. x e. a /\ (a u. {x}) e. ((n +o 1c) +o 1c)) -> a e. (n +o 1c)))
160	159	alrimivv 1632	. . . . 5 |- (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> A.aA.x((-. x e. a /\ (a u. {x}) e. ((n +o 1c) +o 1c)) -> a e. (n +o 1c)))
161	160	a1i 10	. . . 4 |- (n e. Nn -> (A.cA.z((-. z e. c /\ (c u. {z}) e. (n +o 1c)) -> c e. n) -> A.aA.x((-. x e. a /\ (a u. {x}) e. ((n +o 1c) +o 1c)) -> a e. (n +o 1c))))
162	1, 17, 36, 42, 48, 59, 161	finds 4412	. . 3 |- (M e. Nn -> A.aA.x((-. x e. a /\ (a u. {x}) e. (M +o 1c)) -> a e. M))
163		nnsucelr.2	. . . . 5 |- X e. _V
164		eleq1 2413	. . . . . . . 8 |- (x = X -> (x e. a <-> X e. a))
165	164	notbid 285	. . . . . . 7 |- (x = X -> (-. x e. a <-> -. X e. a))
166		sneq 3745	. . . . . . . . 9 |- (x = X -> {x} = {X})
167	166	uneq2d 3419	. . . . . . . 8 |- (x = X -> (a u. {x}) = (a u. {X}))
168	167	eleq1d 2419	. . . . . . 7 |- (x = X -> ((a u. {x}) e. (M +o 1c) <-> (a u. {X}) e. (M +o 1c)))
169	165, 168	anbi12d 691	. . . . . 6 |- (x = X -> ((-. x e. a /\ (a u. {x}) e. (M +o 1c)) <-> (-. X e. a /\ (a u. {X}) e. (M +o 1c))))
170	169	imbi1d 308	. . . . 5 |- (x = X -> (((-. x e. a /\ (a u. {x}) e. (M +o 1c)) -> a e. M) <-> ((-. X e. a /\ (a u. {X}) e. (M +o 1c)) -> a e. M)))
171	163, 170	spcv 2946	. . . 4 |- (A.x((-. x e. a /\ (a u. {x}) e. (M +o 1c)) -> a e. M) -> ((-. X e. a /\ (a u. {X}) e. (M +o 1c)) -> a e. M))
172	171	alimi 1559	. . 3 |- (A.aA.x((-. x e. a /\ (a u. {x}) e. (M +o 1c)) -> a e. M) -> A.a((-. X e. a /\ (a u. {X}) e. (M +o 1c)) -> a e. M))
173		nnsucelr.1	. . . 4 |- A e. _V
174		eleq2 2414	. . . . . . 7 |- (a = A -> (X e. a <-> X e. A))
175	174	notbid 285	. . . . . 6 |- (a = A -> (-. X e. a <-> -. X e. A))
176		uneq1 3412	. . . . . . 7 |- (a = A -> (a u. {X}) = (A u. {X}))
177	176	eleq1d 2419	. . . . . 6 |- (a = A -> ((a u. {X}) e. (M +o 1c) <-> (A u. {X}) e. (M +o 1c)))
178	175, 177	anbi12d 691	. . . . 5 |- (a = A -> ((-. X e. a /\ (a u. {X}) e. (M +o 1c)) <-> (-. X e. A /\ (A u. {X}) e. (M +o 1c))))
179		eleq1 2413	. . . . 5 |- (a = A -> (a e. M <-> A e. M))
180	178, 179	imbi12d 311	. . . 4 |- (a = A -> (((-. X e. a /\ (a u. {X}) e. (M +o 1c)) -> a e. M) <-> ((-. X e. A /\ (A u. {X}) e. (M +o 1c)) -> A e. M)))
181	173, 180	spcv 2946	. . 3 |- (A.a((-. X e. a /\ (a u. {X}) e. (M +o 1c)) -> a e. M) -> ((-. X e. A /\ (A u. {X}) e. (M +o 1c)) -> A e. M))
182	162, 172, 181	3syl 18	. 2 |- (M e. Nn -> ((-. X e. A /\ (A u. {X}) e. (M +o 1c)) -> A e. M))
183	182	imp 418	1 |- ((M e. Nn /\ (-. X e. A /\ (A u. {X}) e. (M +o 1c))) -> A e. M)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710   =/= wne 2517  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   u. cun 3208   C_ wss 3258  (/)c0 3551  {csn 3738  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +o cplc 4376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-0c 4378  df-addc 4379  df-nnc 4380

This theorem is referenced by:  nndisjeq  4430  prepeano4  4452  ssfin  4471