Theorem axfelem11 14041

Description: Lemma for axfe (future) . C is either a limit or successor ordinal.

Hypothesis

Ref	Expression
axfelem11.1	|- C = |^|{a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)}

Assertion

Ref	Expression
axfelem11	|- ((L =/= (/) /\ R =/= (/)) -> ((((L C_ No /\ R C_ No ) /\ (L e. A /\ R e. B)) /\ A.x e. L A.y e. R x <s y) -> (E.d e. On C = suc d \/ Lim C)))

Distinct variable groups:   C,d   L,a,p,q   x,L,p   y,p   x,q,y   R,a,p,q   x,R,y

Proof of Theorem axfelem11

Step	Hyp	Ref	Expression
1		eqid 1884	. . . . . . . . . . . 12 |- (/) = (/)
2	1	jctr 315	. . . . . . . . . . 11 |- (p e. L -> (p e. L /\ (/) = (/)))
3	2	anim1i 361	. . . . . . . . . 10 |- ((p e. L /\ q e. R) -> ((p e. L /\ (/) = (/)) /\ q e. R))
4	3	ancomd 483	. . . . . . . . 9 |- ((p e. L /\ q e. R) -> (q e. R /\ (p e. L /\ (/) = (/))))
5	4	2eximi 1388	. . . . . . . 8 |- (E.pE.q(p e. L /\ q e. R) -> E.pE.q(q e. R /\ (p e. L /\ (/) = (/))))
6		df-rex 2110	. . . . . . . . 9 |- (E.p e. L E.q e. R (/) = (/) <-> E.p(p e. L /\ E.q e. R (/) = (/)))
7		r19.42v 2237	. . . . . . . . . 10 |- (E.q e. R (p e. L /\ (/) = (/)) <-> (p e. L /\ E.q e. R (/) = (/)))
8	7	exbii 1398	. . . . . . . . 9 |- (E.pE.q e. R (p e. L /\ (/) = (/)) <-> E.p(p e. L /\ E.q e. R (/) = (/)))
9		df-rex 2110	. . . . . . . . . 10 |- (E.q e. R (p e. L /\ (/) = (/)) <-> E.q(q e. R /\ (p e. L /\ (/) = (/))))
10	9	exbii 1398	. . . . . . . . 9 |- (E.pE.q e. R (p e. L /\ (/) = (/)) <-> E.pE.q(q e. R /\ (p e. L /\ (/) = (/))))
11	6, 8, 10	3bitr2i 196	. . . . . . . 8 |- (E.p e. L E.q e. R (/) = (/) <-> E.pE.q(q e. R /\ (p e. L /\ (/) = (/))))
12	5, 11	sylibr 217	. . . . . . 7 |- (E.pE.q(p e. L /\ q e. R) -> E.p e. L E.q e. R (/) = (/))
13		n0 2884	. . . . . . . . 9 |- (L =/= (/) <-> E.p p e. L)
14		n0 2884	. . . . . . . . 9 |- (R =/= (/) <-> E.q q e. R)
15	13, 14	anbi12i 540	. . . . . . . 8 |- ((L =/= (/) /\ R =/= (/)) <-> (E.p p e. L /\ E.q q e. R))
16		eeanv 1707	. . . . . . . 8 |- (E.pE.q(p e. L /\ q e. R) <-> (E.p p e. L /\ E.q q e. R))
17	15, 16	bitr4i 193	. . . . . . 7 |- ((L =/= (/) /\ R =/= (/)) <-> E.pE.q(p e. L /\ q e. R))
18		rexnal 2114	. . . . . . . 8 |- (E.p e. L -. A.q e. R (/) =/= (/) <-> -. A.p e. L A.q e. R (/) =/= (/))
19		df-ne 2019	. . . . . . . . . . . 12 |- ((/) =/= (/) <-> -. (/) = (/))
20	19	con2bii 238	. . . . . . . . . . 11 |- ((/) = (/) <-> -. (/) =/= (/))
21	20	rexbii 2128	. . . . . . . . . 10 |- (E.q e. R (/) = (/) <-> E.q e. R -. (/) =/= (/))
22		rexnal 2114	. . . . . . . . . 10 |- (E.q e. R -. (/) =/= (/) <-> -. A.q e. R (/) =/= (/))
23	21, 22	bitr2i 191	. . . . . . . . 9 |- (-. A.q e. R (/) =/= (/) <-> E.q e. R (/) = (/))
24	23	rexbii 2128	. . . . . . . 8 |- (E.p e. L -. A.q e. R (/) =/= (/) <-> E.p e. L E.q e. R (/) = (/))
25	18, 24	bitr3i 192	. . . . . . 7 |- (-. A.p e. L A.q e. R (/) =/= (/) <-> E.p e. L E.q e. R (/) = (/))
26	12, 17, 25	3imtr4i 236	. . . . . 6 |- ((L =/= (/) /\ R =/= (/)) -> -. A.p e. L A.q e. R (/) =/= (/))
27		reseq2 4219	. . . . . . . . . . . 12 |- (a = (/) -> (p |` a) = (p |` (/)))
28		reseq2 4219	. . . . . . . . . . . 12 |- (a = (/) -> (q |` a) = (q |` (/)))
29	27, 28	eqeq12d 1899	. . . . . . . . . . 11 |- (a = (/) -> ((p |` a) = (q |` a) <-> (p |` (/)) = (q |` (/))))
30		res0 4221	. . . . . . . . . . . 12 |- (p |` (/)) = (/)
31		res0 4221	. . . . . . . . . . . 12 |- (q |` (/)) = (/)
32	30, 31	eqeq12i 1897	. . . . . . . . . . 11 |- ((p |` (/)) = (q |` (/)) <-> (/) = (/))
33	29, 32	syl6bb 595	. . . . . . . . . 10 |- (a = (/) -> ((p |` a) = (q |` a) <-> (/) = (/)))
34	33	necon3bid 2035	. . . . . . . . 9 |- (a = (/) -> ((p |` a) =/= (q |` a) <-> (/) =/= (/)))
35	34	2ralbidv 2140	. . . . . . . 8 |- (a = (/) -> (A.p e. L A.q e. R (p |` a) =/= (q |` a) <-> A.p e. L A.q e. R (/) =/= (/)))
36	35	elrab 2414	. . . . . . 7 |- ((/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} <-> ((/) e. On /\ A.p e. L A.q e. R (/) =/= (/)))
37	36	simprbi 353	. . . . . 6 |- ((/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} -> A.p e. L A.q e. R (/) =/= (/))
38	26, 37	nsyl 131	. . . . 5 |- ((L =/= (/) /\ R =/= (/)) -> -. (/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)})
39		axfelem11.1	. . . . . . . 8 |- C = |^|{a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)}
40	39	eqeq1i 1891	. . . . . . 7 |- (C = (/) <-> |^|{a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} = (/))
41		ssrab2 2692	. . . . . . . 8 |- {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} C_ On
42		onint0 3877	. . . . . . . 8 |- ({a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} C_ On -> (|^|{a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} = (/) <-> (/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)}))
43	41, 42	ax-mp 7	. . . . . . 7 |- (|^|{a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)} = (/) <-> (/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)})
44	40, 43	bitri 190	. . . . . 6 |- (C = (/) <-> (/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)})
45	44	notbii 204	. . . . 5 |- (-. C = (/) <-> -. (/) e. {a e. On | A.p e. L A.q e. R (p |` a) =/= (q |` a)})
46	38, 45	sylibr 217	. . . 4 |- ((L =/= (/) /\ R =/= (/)) -> -. C = (/))
47		3orel1 13805	. . . 4 |- (-. C = (/) -> ((C = (/) \/ E.d e. On C = suc d \/ Lim C) -> (E.d e. On C = suc d \/ Lim C)))
48	46, 47	syl 12	. . 3 |- ((L =/= (/) /\ R =/= (/)) -> ((C = (/) \/ E.d e. On C = suc d \/ Lim C) -> (E.d e. On C = suc d \/ Lim C)))
49		eloni 3667	. . . 4 |- (C e. On -> Ord C)
50		ordzsl 3927	. . . 4 |- (Ord C <-> (C = (/) \/ E.d e. On C = suc d \/ Lim C))
51	49, 50	sylib 215	. . 3 |- (C e. On -> (C = (/) \/ E.d e. On C = suc d \/ Lim C))
52	48, 51	syl5 20	. 2 |- ((L =/= (/) /\ R =/= (/)) -> (C e. On -> (E.d e. On C = suc d \/ Lim C)))
53	39	axfelem10 14040	. 2 |- ((((L C_ No /\ R C_ No ) /\ (L e. A /\ R e. B)) /\ A.x e. L A.y e. R x <s y) -> C e. On)
54	52, 53	syl5 20	1 |- ((L =/= (/) /\ R =/= (/)) -> ((((L C_ No /\ R C_ No ) /\ (L e. A /\ R e. B)) /\ A.x e. L A.y e. R x <s y) -> (E.d e. On C = suc d \/ Lim C)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   C_ wss 2593  (/)c0 2875  |^|cint 3214   class class class wbr 3338  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659   |` cres 3988   No csur 13981   <s cslt 13982

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-if 2983  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-lim 3662  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