Theorem nmembers1lem3 6270

Description: Lemma for nmembers1 6271. If the interval from one to a natural is in a given natural, extending it by one puts it in the next natural. (Contributed by Scott Fenton, 3-Aug-2019.)

Assertion

Ref	Expression
nmembers1lem3	|- ((A e. Nn /\ B e. Nn ) -> ({m e. Nn | (1c <_c m /\ m <_c A)} e. B -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c)))

Distinct variable groups:   A,m   B,m

Proof of Theorem nmembers1lem3

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnltp1c 6262	. . . . . . . . . . . 12 |- (A e. Nn -> A <c (A +o 1c))
2		nnnc 6146	. . . . . . . . . . . . 13 |- (A e. Nn -> A e. NC )
3		peano2 4403	. . . . . . . . . . . . . 14 |- (A e. Nn -> (A +o 1c) e. Nn )
4		nnnc 6146	. . . . . . . . . . . . . 14 |- ((A +o 1c) e. Nn -> (A +o 1c) e. NC )
5	3, 4	syl 15	. . . . . . . . . . . . 13 |- (A e. Nn -> (A +o 1c) e. NC )
6		ltlenlec 6207	. . . . . . . . . . . . 13 |- ((A e. NC /\ (A +o 1c) e. NC ) -> (A <c (A +o 1c) <-> (A <_c (A +o 1c) /\ -. (A +o 1c) <_c A)))
7	2, 5, 6	syl2anc 642	. . . . . . . . . . . 12 |- (A e. Nn -> (A <c (A +o 1c) <-> (A <_c (A +o 1c) /\ -. (A +o 1c) <_c A)))
8	1, 7	mpbid 201	. . . . . . . . . . 11 |- (A e. Nn -> (A <_c (A +o 1c) /\ -. (A +o 1c) <_c A))
9	8	simprd 449	. . . . . . . . . 10 |- (A e. Nn -> -. (A +o 1c) <_c A)
10	9	adantr 451	. . . . . . . . 9 |- ((A e. Nn /\ B e. Nn ) -> -. (A +o 1c) <_c A)
11	10	intnand 882	. . . . . . . 8 |- ((A e. Nn /\ B e. Nn ) -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A))
12	11	a1d 22	. . . . . . 7 |- ((A e. Nn /\ B e. Nn ) -> ((A +o 1c) e. Nn -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
13		breq2 4643	. . . . . . . . . . 11 |- (m = (A +o 1c) -> (1c <_c m <-> 1c <_c (A +o 1c)))
14		breq1 4642	. . . . . . . . . . 11 |- (m = (A +o 1c) -> (m <_c A <-> (A +o 1c) <_c A))
15	13, 14	anbi12d 691	. . . . . . . . . 10 |- (m = (A +o 1c) -> ((1c <_c m /\ m <_c A) <-> (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
16	15	elrab 2994	. . . . . . . . 9 |- ((A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> ((A +o 1c) e. Nn /\ (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
17	16	notbii 287	. . . . . . . 8 |- (-. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> -. ((A +o 1c) e. Nn /\ (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
18		imnan 411	. . . . . . . 8 |- (((A +o 1c) e. Nn -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)) <-> -. ((A +o 1c) e. Nn /\ (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
19	17, 18	bitr4i 243	. . . . . . 7 |- (-. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> ((A +o 1c) e. Nn -> -. (1c <_c (A +o 1c) /\ (A +o 1c) <_c A)))
20	12, 19	sylibr 203	. . . . . 6 |- ((A e. Nn /\ B e. Nn ) -> -. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)})
21	3	adantr 451	. . . . . . 7 |- ((A e. Nn /\ B e. Nn ) -> (A +o 1c) e. Nn )
22		elcomplg 3218	. . . . . . 7 |- ((A +o 1c) e. Nn -> ((A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} <-> -. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)}))
23	21, 22	syl 15	. . . . . 6 |- ((A e. Nn /\ B e. Nn ) -> ((A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} <-> -. (A +o 1c) e. {m e. Nn | (1c <_c m /\ m <_c A)}))
24	20, 23	mpbird 223	. . . . 5 |- ((A e. Nn /\ B e. Nn ) -> (A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)})
25		nnnc 6146	. . . . . . . . . . . . . 14 |- (x e. Nn -> x e. NC )
26		ncslesuc 6267	. . . . . . . . . . . . . 14 |- ((x e. NC /\ A e. NC ) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c))))
27	25, 2, 26	syl2an 463	. . . . . . . . . . . . 13 |- ((x e. Nn /\ A e. Nn ) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c))))
28	27	expcom 424	. . . . . . . . . . . 12 |- (A e. Nn -> (x e. Nn -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c)))))
29	28	adantrd 454	. . . . . . . . . . 11 |- (A e. Nn -> ((x e. Nn /\ 1c <_c x) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c)))))
30	29	adantr 451	. . . . . . . . . 10 |- ((A e. Nn /\ B e. Nn ) -> ((x e. Nn /\ 1c <_c x) -> (x <_c (A +o 1c) <-> (x <_c A \/ x = (A +o 1c)))))
31	30	pm5.32d 620	. . . . . . . . 9 |- ((A e. Nn /\ B e. Nn ) -> (((x e. Nn /\ 1c <_c x) /\ x <_c (A +o 1c)) <-> ((x e. Nn /\ 1c <_c x) /\ (x <_c A \/ x = (A +o 1c)))))
32		anass 630	. . . . . . . . 9 |- (((x e. Nn /\ 1c <_c x) /\ x <_c (A +o 1c)) <-> (x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))))
33		andi 837	. . . . . . . . . 10 |- (((x e. Nn /\ 1c <_c x) /\ (x <_c A \/ x = (A +o 1c))) <-> (((x e. Nn /\ 1c <_c x) /\ x <_c A) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
34		anass 630	. . . . . . . . . . 11 |- (((x e. Nn /\ 1c <_c x) /\ x <_c A) <-> (x e. Nn /\ (1c <_c x /\ x <_c A)))
35	34	orbi1i 506	. . . . . . . . . 10 |- ((((x e. Nn /\ 1c <_c x) /\ x <_c A) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
36	33, 35	bitri 240	. . . . . . . . 9 |- (((x e. Nn /\ 1c <_c x) /\ (x <_c A \/ x = (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
37	31, 32, 36	3bitr3g 278	. . . . . . . 8 |- ((A e. Nn /\ B e. Nn ) -> ((x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c)))))
38		1cnc 6139	. . . . . . . . . . . . . . . 16 |- 1c e. NC
39		addlecncs 6209	. . . . . . . . . . . . . . . 16 |- ((1c e. NC /\ A e. NC ) -> 1c <_c (1c +o A))
40	38, 2, 39	sylancr 644	. . . . . . . . . . . . . . 15 |- (A e. Nn -> 1c <_c (1c +o A))
41		addccom 4406	. . . . . . . . . . . . . . 15 |- (A +o 1c) = (1c +o A)
42	40, 41	syl6breqr 4679	. . . . . . . . . . . . . 14 |- (A e. Nn -> 1c <_c (A +o 1c))
43	3, 42	jca 518	. . . . . . . . . . . . 13 |- (A e. Nn -> ((A +o 1c) e. Nn /\ 1c <_c (A +o 1c)))
44		eleq1 2413	. . . . . . . . . . . . . 14 |- (x = (A +o 1c) -> (x e. Nn <-> (A +o 1c) e. Nn ))
45		breq2 4643	. . . . . . . . . . . . . 14 |- (x = (A +o 1c) -> (1c <_c x <-> 1c <_c (A +o 1c)))
46	44, 45	anbi12d 691	. . . . . . . . . . . . 13 |- (x = (A +o 1c) -> ((x e. Nn /\ 1c <_c x) <-> ((A +o 1c) e. Nn /\ 1c <_c (A +o 1c))))
47	43, 46	syl5ibrcom 213	. . . . . . . . . . . 12 |- (A e. Nn -> (x = (A +o 1c) -> (x e. Nn /\ 1c <_c x)))
48	47	adantr 451	. . . . . . . . . . 11 |- ((A e. Nn /\ B e. Nn ) -> (x = (A +o 1c) -> (x e. Nn /\ 1c <_c x)))
49	48	pm4.71rd 616	. . . . . . . . . 10 |- ((A e. Nn /\ B e. Nn ) -> (x = (A +o 1c) <-> ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))))
50	49	bicomd 192	. . . . . . . . 9 |- ((A e. Nn /\ B e. Nn ) -> (((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c)) <-> x = (A +o 1c)))
51	50	orbi2d 682	. . . . . . . 8 |- ((A e. Nn /\ B e. Nn ) -> (((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ ((x e. Nn /\ 1c <_c x) /\ x = (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c))))
52	37, 51	bitrd 244	. . . . . . 7 |- ((A e. Nn /\ B e. Nn ) -> ((x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c))))
53		breq2 4643	. . . . . . . . 9 |- (m = x -> (1c <_c m <-> 1c <_c x))
54		breq1 4642	. . . . . . . . 9 |- (m = x -> (m <_c (A +o 1c) <-> x <_c (A +o 1c)))
55	53, 54	anbi12d 691	. . . . . . . 8 |- (m = x -> ((1c <_c m /\ m <_c (A +o 1c)) <-> (1c <_c x /\ x <_c (A +o 1c))))
56	55	elrab 2994	. . . . . . 7 |- (x e. {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} <-> (x e. Nn /\ (1c <_c x /\ x <_c (A +o 1c))))
57		elun 3220	. . . . . . . 8 |- (x e. ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}) <-> (x e. {m e. Nn | (1c <_c m /\ m <_c A)} \/ x e. {(A +o 1c)}))
58		breq1 4642	. . . . . . . . . . 11 |- (m = x -> (m <_c A <-> x <_c A))
59	53, 58	anbi12d 691	. . . . . . . . . 10 |- (m = x -> ((1c <_c m /\ m <_c A) <-> (1c <_c x /\ x <_c A)))
60	59	elrab 2994	. . . . . . . . 9 |- (x e. {m e. Nn | (1c <_c m /\ m <_c A)} <-> (x e. Nn /\ (1c <_c x /\ x <_c A)))
61		elsn 3748	. . . . . . . . 9 |- (x e. {(A +o 1c)} <-> x = (A +o 1c))
62	60, 61	orbi12i 507	. . . . . . . 8 |- ((x e. {m e. Nn | (1c <_c m /\ m <_c A)} \/ x e. {(A +o 1c)}) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c)))
63	57, 62	bitri 240	. . . . . . 7 |- (x e. ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}) <-> ((x e. Nn /\ (1c <_c x /\ x <_c A)) \/ x = (A +o 1c)))
64	52, 56, 63	3bitr4g 279	. . . . . 6 |- ((A e. Nn /\ B e. Nn ) -> (x e. {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} <-> x e. ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)})))
65	64	eqrdv 2351	. . . . 5 |- ((A e. Nn /\ B e. Nn ) -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}))
66		sneq 3744	. . . . . . . 8 |- (y = (A +o 1c) -> {y} = {(A +o 1c)})
67	66	uneq2d 3418	. . . . . . 7 |- (y = (A +o 1c) -> ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}) = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)}))
68	67	eqeq2d 2364	. . . . . 6 |- (y = (A +o 1c) -> ({m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}) <-> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)})))
69	68	rspcev 2955	. . . . 5 |- (((A +o 1c) e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} /\ {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {(A +o 1c)})) -> E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}))
70	24, 65, 69	syl2anc 642	. . . 4 |- ((A e. Nn /\ B e. Nn ) -> E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}))
71		compleq 3243	. . . . . 6 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> ∼ x = ∼ {m e. Nn | (1c <_c m /\ m <_c A)})
72		uneq1 3411	. . . . . . 7 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> (x u. {y}) = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y}))
73	72	eqeq2d 2364	. . . . . 6 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> ({m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}) <-> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y})))
74	71, 73	rexeqbidv 2820	. . . . 5 |- (x = {m e. Nn | (1c <_c m /\ m <_c A)} -> (E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}) <-> E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y})))
75	74	rspcev 2955	. . . 4 |- (({m e. Nn | (1c <_c m /\ m <_c A)} e. B /\ E.y e. ∼ {m e. Nn | (1c <_c m /\ m <_c A)} {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = ({m e. Nn | (1c <_c m /\ m <_c A)} u. {y})) -> E.x e. B E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}))
76	70, 75	sylan2 460	. . 3 |- (({m e. Nn | (1c <_c m /\ m <_c A)} e. B /\ (A e. Nn /\ B e. Nn )) -> E.x e. B E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}))
77		elsuc 4413	. . 3 |- ({m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c) <-> E.x e. B E.y e. ∼ x{m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} = (x u. {y}))
78	76, 77	sylibr 203	. 2 |- (({m e. Nn | (1c <_c m /\ m <_c A)} e. B /\ (A e. Nn /\ B e. Nn )) -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c))
79	78	expcom 424	1 |- ((A e. Nn /\ B e. Nn ) -> ({m e. Nn | (1c <_c m /\ m <_c A)} e. B -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   = wceq 1642   e. wcel 1710  E.wrex 2615  {crab 2618   ∼ ccompl 3205   u. cun 3207  {csn 3737  1_cc1c 4134   Nn cnnc 4373   +o cplc 4375   class class class wbr 4639   NC cncs 6088   <__c clec 6089   <_c cltc 6090

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-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-csb 3137  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-fix 5740  df-cup 5742  df-disj 5744  df-addcfn 5746  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-clos1 5873  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-en 6029  df-ncs 6098  df-lec 6099  df-ltc 6100  df-nc 6101

This theorem is referenced by:  nmembers1  6271