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 ∈ V
nnsucelr.2	⊢ X ∈ V

Assertion

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710   ≠ wne 2517  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∖ cdif 3207   ∪ cun 3208   ⊆ wss 3258  ∅c0 3551  {csn 3738  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +_c 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