Theorem axdenselem8 14026

Description: Lemma for axdense 14027. Give a condition for surreal less than when two surreals have the same birthday.

Assertion

Ref	Expression
axdenselem8	|- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (A <s B <-> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))

Distinct variable groups:   A,a   B,a

Proof of Theorem axdenselem8

Step	Hyp	Ref	Expression
1		axdenselem5 14023	. . . . 5 |- (((A e. No /\ B e. No ) /\ (( bday ` A) = ( bday ` B) /\ A <s B)) -> |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A))
2	1	exp32 408	. . . 4 |- ((A e. No /\ B e. No ) -> (( bday ` A) = ( bday ` B) -> (A <s B -> |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A))))
3	2	3impia 1064	. . 3 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (A <s B -> |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)))
4		sltval2 13997	. . . . 5 |- ((A e. No /\ B e. No ) -> (A <s B <-> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
5	4	3adant3 896	. . . 4 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (A <s B <-> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
6		eleq2 1958	. . . . . . . . . . . . 13 |- (( bday ` A) = ( bday ` B) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) <-> |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)))
7	6	biimpd 170	. . . . . . . . . . . 12 |- (( bday ` A) = ( bday ` B) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)))
8		nosgnn0 13999	. . . . . . . . . . . . . . 15 |- -. (/) e. {1o, 2o}
9		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> ((B` |^|{a e. On | (A` a) =/= (B` a)}) e. ran B <-> (/) e. ran B))
10		fnfvelrn 4786	. . . . . . . . . . . . . . . . . 18 |- ((B Fn ( bday ` B) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)) -> (B` |^|{a e. On | (A` a) =/= (B` a)}) e. ran B)
11	9, 10	syl5cbi 226	. . . . . . . . . . . . . . . . 17 |- ((B Fn ( bday ` B) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)) -> ((B` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> (/) e. ran B))
12		axdenselem1 14019	. . . . . . . . . . . . . . . . 17 |- (B e. No -> B Fn ( bday ` B))
13	11, 12	sylan 497	. . . . . . . . . . . . . . . 16 |- ((B e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)) -> ((B` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> (/) e. ran B))
14		norn 13995	. . . . . . . . . . . . . . . . . 18 |- (B e. No -> ran B C_ {1o, 2o})
15	14	sseld 2619	. . . . . . . . . . . . . . . . 17 |- (B e. No -> ((/) e. ran B -> (/) e. {1o, 2o}))
16	15	adantr 425	. . . . . . . . . . . . . . . 16 |- ((B e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)) -> ((/) e. ran B -> (/) e. {1o, 2o}))
17	13, 16	syld 30	. . . . . . . . . . . . . . 15 |- ((B e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)) -> ((B` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> (/) e. {1o, 2o}))
18	8, 17	mtoi 122	. . . . . . . . . . . . . 14 |- ((B e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B)) -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
19	18	ex 402	. . . . . . . . . . . . 13 |- (B e. No -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B) -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)))
20	19	adantl 424	. . . . . . . . . . . 12 |- ((A e. No /\ B e. No ) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` B) -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)))
21	7, 20	syl9r 72	. . . . . . . . . . 11 |- ((A e. No /\ B e. No ) -> (( bday ` A) = ( bday ` B) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))))
22	21	3impia 1064	. . . . . . . . . 10 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)))
23	22	imp 377	. . . . . . . . 9 |- (((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
24	23	intnand 757	. . . . . . . 8 |- (((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> -. ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)))
25		eleq1 1957	. . . . . . . . . . . . . 14 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) e. ran A <-> (/) e. ran A))
26		fnfvelrn 4786	. . . . . . . . . . . . . 14 |- ((A Fn ( bday ` A) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> (A` |^|{a e. On | (A` a) =/= (B` a)}) e. ran A)
27	25, 26	syl5cbi 226	. . . . . . . . . . . . 13 |- ((A Fn ( bday ` A) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> (/) e. ran A))
28		axdenselem1 14019	. . . . . . . . . . . . 13 |- (A e. No -> A Fn ( bday ` A))
29	27, 28	sylan 497	. . . . . . . . . . . 12 |- ((A e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> (/) e. ran A))
30		norn 13995	. . . . . . . . . . . . . 14 |- (A e. No -> ran A C_ {1o, 2o})
31	30	sseld 2619	. . . . . . . . . . . . 13 |- (A e. No -> ((/) e. ran A -> (/) e. {1o, 2o}))
32	31	adantr 425	. . . . . . . . . . . 12 |- ((A e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> ((/) e. ran A -> (/) e. {1o, 2o}))
33	29, 32	syld 30	. . . . . . . . . . 11 |- ((A e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) -> (/) e. {1o, 2o}))
34	8, 33	mtoi 122	. . . . . . . . . 10 |- ((A e. No /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> -. (A` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
35	34	3ad2antl1 1038	. . . . . . . . 9 |- (((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> -. (A` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
36	35	intnanrd 758	. . . . . . . 8 |- (((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> -. ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o))
37		3orel13 13816	. . . . . . . 8 |- ((-. ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) /\ -. ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)) -> ((((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))
38	24, 36, 37	syl11anc 524	. . . . . . 7 |- (((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) /\ |^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A)) -> ((((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))
39	38	ex 402	. . . . . 6 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> ((((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o))))
40	39	com23 36	. . . . 5 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> ((((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o))))
41		fvex 4689	. . . . . 6 |- (A` |^|{a e. On | (A` a) =/= (B` a)}) e. _V
42		fvex 4689	. . . . . 6 |- (B` |^|{a e. On | (A` a) =/= (B` a)}) e. _V
43		0ex 3446	. . . . . 6 |- (/) e. _V
44		2on 5183	. . . . . . 7 |- 2o e. On
45	44	elisseti 2301	. . . . . 6 |- 2o e. _V
46	41, 42, 43, 45, 45	brtp 13830	. . . . 5 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}) <-> (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))
47	40, 46	syl5ib 223	. . . 4 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}) -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o))))
48	5, 47	sylbid 220	. . 3 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (A <s B -> (|^|{a e. On | (A` a) =/= (B` a)} e. ( bday ` A) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o))))
49	3, 48	mpdd 57	. 2 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (A <s B -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))
50		3mix2 1046	. . . 4 |- (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) -> (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) \/ ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))
51	50, 46	sylibr 217	. . 3 |- (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) -> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))
52	5, 51	syl5bir 227	. 2 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) -> A <s B))
53	49, 52	impbid 574	1 |- ((A e. No /\ B e. No /\ ( bday ` A) = ( bday ` B)) -> (A <s B <-> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  {crab 2108  (/)c0 2875  {cpr 3045  <.cop 3046  {ctp 3051  |^|cint 3214   class class class wbr 3338  Oncon0 3657  ran crn 3987   Fn wfn 3993  ` cfv 3998  1oc1o 5172  2oc2o 5173   No csur 13981   <s cslt 13982   bday cbday 13983

This theorem is referenced by:  axdense 14027

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-suc 3663  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-mpt 5006  df-1o 5177  df-2o 5178  df-no 13984  df-slt 13985  df-bday 13986

Copyright terms: Public domain