Theorem sltval2 13997

Description: Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ.

Assertion

Ref	Expression
sltval2	|- ((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)})))

Distinct variable groups:   A,a   B,a

Proof of Theorem sltval2

Step	Hyp	Ref	Expression
1		sltval 13988	. 2 |- ((A e. No /\ B e. No ) -> (A <s B <-> E.x e. On (A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x))))
2		fvex 4689	. . . . . . . . . . . . 13 |- (A` |^|{a e. On | (A` a) =/= (B` a)}) e. _V
3		fvex 4689	. . . . . . . . . . . . 13 |- (B` |^|{a e. On | (A` a) =/= (B` a)}) e. _V
4		0ex 3446	. . . . . . . . . . . . 13 |- (/) e. _V
5		2on 5183	. . . . . . . . . . . . . 14 |- 2o e. On
6	5	elisseti 2301	. . . . . . . . . . . . 13 |- 2o e. _V
7	2, 3, 4, 6, 6	brtp 13830	. . . . . . . . . . . 12 |- ((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)))
8		1n0 5187	. . . . . . . . . . . . . . . . 17 |- 1o =/= (/)
9		df-ne 2019	. . . . . . . . . . . . . . . . 17 |- (1o =/= (/) <-> -. 1o = (/))
10	8, 9	mpbi 206	. . . . . . . . . . . . . . . 16 |- -. 1o = (/)
11		eqeq1 1890	. . . . . . . . . . . . . . . 16 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) <-> 1o = (/)))
12	10, 11	mtbiri 785	. . . . . . . . . . . . . . 15 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o -> -. (A` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
13		fvprc 4678	. . . . . . . . . . . . . . 15 |- (-. |^|{a e. On | (A` a) =/= (B` a)} e. _V -> (A` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
14	12, 13	nsyl2 133	. . . . . . . . . . . . . 14 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o -> |^|{a e. On | (A` a) =/= (B` a)} e. _V)
15	14	adantr 425	. . . . . . . . . . . . 13 |- (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/)) -> |^|{a e. On | (A` a) =/= (B` a)} e. _V)
16	14	adantr 425	. . . . . . . . . . . . 13 |- (((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o /\ (B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o) -> |^|{a e. On | (A` a) =/= (B` a)} e. _V)
17		2on0 13862	. . . . . . . . . . . . . . . . 17 |- 2o =/= (/)
18		df-ne 2019	. . . . . . . . . . . . . . . . 17 |- (2o =/= (/) <-> -. 2o = (/))
19	17, 18	mpbi 206	. . . . . . . . . . . . . . . 16 |- -. 2o = (/)
20		eqeq1 1890	. . . . . . . . . . . . . . . 16 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o -> ((B` |^|{a e. On | (A` a) =/= (B` a)}) = (/) <-> 2o = (/)))
21	19, 20	mtbiri 785	. . . . . . . . . . . . . . 15 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
22		fvprc 4678	. . . . . . . . . . . . . . 15 |- (-. |^|{a e. On | (A` a) =/= (B` a)} e. _V -> (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
23	21, 22	nsyl2 133	. . . . . . . . . . . . . 14 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o -> |^|{a e. On | (A` a) =/= (B` a)} e. _V)
24	23	adantl 424	. . . . . . . . . . . . 13 |- (((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. _V)
25	15, 16, 24	3jaoi 1160	. . . . . . . . . . . 12 |- ((((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. _V)
26	7, 25	sylbi 216	. . . . . . . . . . 11 |- ((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. _V)
27		onintrab 3882	. . . . . . . . . . 11 |- (|^|{a e. On | (A` a) =/= (B` a)} e. _V <-> |^|{a e. On | (A` a) =/= (B` a)} e. On)
28	26, 27	sylib 215	. . . . . . . . . 10 |- ((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. On)
29	28	adantl 424	. . . . . . . . 9 |- (((A e. No /\ B e. No ) /\ (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. On)
30		onelon 3683	. . . . . . . . . . . . . . 15 |- ((|^|{a e. On | (A` a) =/= (B` a)} e. On /\ y e. |^|{a e. On | (A` a) =/= (B` a)}) -> y e. On)
31	30	expcom 403	. . . . . . . . . . . . . 14 |- (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (|^|{a e. On | (A` a) =/= (B` a)} e. On -> y e. On))
32	31, 29	syl5 20	. . . . . . . . . . . . 13 |- (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (((A e. No /\ B e. No ) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})) -> y e. On))
33		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (a = y -> (A` a) = (A` y))
34		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (a = y -> (B` a) = (B` y))
35	33, 34	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (a = y -> ((A` a) = (B` a) <-> (A` y) = (B` y)))
36	35	necon3bid 2035	. . . . . . . . . . . . . . 15 |- (a = y -> ((A` a) =/= (B` a) <-> (A` y) =/= (B` y)))
37	36	onnminsb 3885	. . . . . . . . . . . . . 14 |- (y e. On -> (y e. |^|{a e. On | (A` a) =/= (B` a)} -> -. (A` y) =/= (B` y)))
38	37	com12 14	. . . . . . . . . . . . 13 |- (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (y e. On -> -. (A` y) =/= (B` y)))
39	32, 38	syld 30	. . . . . . . . . . . 12 |- (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (((A e. No /\ B e. No ) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})) -> -. (A` y) =/= (B` y)))
40	39	com12 14	. . . . . . . . . . 11 |- (((A e. No /\ B e. No ) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})) -> (y e. |^|{a e. On | (A` a) =/= (B` a)} -> -. (A` y) =/= (B` y)))
41		df-ne 2019	. . . . . . . . . . . 12 |- ((A` y) =/= (B` y) <-> -. (A` y) = (B` y))
42	41	con2bii 238	. . . . . . . . . . 11 |- ((A` y) = (B` y) <-> -. (A` y) =/= (B` y))
43	40, 42	syl6ibr 230	. . . . . . . . . 10 |- (((A e. No /\ B e. No ) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})) -> (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (A` y) = (B` y)))
44	43	r19.21aiv 2175	. . . . . . . . 9 |- (((A e. No /\ B e. No ) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})) -> A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y))
45	29, 44	jca 310	. . . . . . . 8 |- (((A e. No /\ B e. No ) /\ (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. On /\ A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y)))
46	45	ex 402	. . . . . . 7 |- ((A e. No /\ B e. No ) -> ((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. On /\ A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y))))
47	46	impac 423	. . . . . 6 |- (((A e. No /\ B e. No ) /\ (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. On /\ A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y)) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
48		anass 487	. . . . . 6 |- (((|^|{a e. On | (A` a) =/= (B` a)} e. On /\ A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y)) /\ (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. On /\ (A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))))
49	47, 48	sylib 215	. . . . 5 |- (((A e. No /\ B e. No ) /\ (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. On /\ (A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))))
50		raleq 2266	. . . . . . 7 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> (A.y e. x (A` y) = (B` y) <-> A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y)))
51		fveq2 4681	. . . . . . . 8 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> (A` x) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
52		fveq2 4681	. . . . . . . 8 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> (B` x) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
53	51, 52	breq12d 3351	. . . . . . 7 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) <-> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
54	50, 53	anbi12d 690	. . . . . 6 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> ((A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) <-> (A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))))
55	54	rcla4ev 2381	. . . . 5 |- ((|^|{a e. On | (A` a) =/= (B` a)} e. On /\ (A.y e. |^|{a e. On | (A` a) =/= (B` a)} (A` y) = (B` y) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))) -> E.x e. On (A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)))
56	49, 55	syl 12	. . . 4 |- (((A e. No /\ B e. No ) /\ (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})) -> E.x e. On (A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)))
57	56	ex 402	. . 3 |- ((A e. No /\ B e. No ) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}) -> E.x e. On (A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x))))
58		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (a = x -> (A` a) = (A` x))
59		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (a = x -> (B` a) = (B` x))
60	58, 59	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (a = x -> ((A` a) = (B` a) <-> (A` x) = (B` x)))
61	60	necon3bid 2035	. . . . . . . . . . . . . . 15 |- (a = x -> ((A` a) =/= (B` a) <-> (A` x) =/= (B` x)))
62	61	elrab 2414	. . . . . . . . . . . . . 14 |- (x e. {a e. On | (A` a) =/= (B` a)} <-> (x e. On /\ (A` x) =/= (B` x)))
63	62	biimpri 169	. . . . . . . . . . . . 13 |- ((x e. On /\ (A` x) =/= (B` x)) -> x e. {a e. On | (A` a) =/= (B` a)})
64	63	adantlr 429	. . . . . . . . . . . 12 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x) =/= (B` x)) -> x e. {a e. On | (A` a) =/= (B` a)})
65		onint 3876	. . . . . . . . . . . . . . . . . 18 |- (({a e. On | (A` a) =/= (B` a)} C_ On /\ {a e. On | (A` a) =/= (B` a)} =/= (/)) -> |^|{a e. On | (A` a) =/= (B` a)} e. {a e. On | (A` a) =/= (B` a)})
66		ssrab2 2692	. . . . . . . . . . . . . . . . . 18 |- {a e. On | (A` a) =/= (B` a)} C_ On
67		ne0i 2881	. . . . . . . . . . . . . . . . . . 19 |- (x e. {a e. On | (A` a) =/= (B` a)} -> {a e. On | (A` a) =/= (B` a)} =/= (/))
68	67	adantl 424	. . . . . . . . . . . . . . . . . 18 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> {a e. On | (A` a) =/= (B` a)} =/= (/))
69	65, 66, 68	sylancr 526	. . . . . . . . . . . . . . . . 17 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> |^|{a e. On | (A` a) =/= (B` a)} e. {a e. On | (A` a) =/= (B` a)})
70		hbrab1 2257	. . . . . . . . . . . . . . . . . . . 20 |- (x e. {a e. On | (A` a) =/= (B` a)} -> A.a x e. {a e. On | (A` a) =/= (B` a)})
71	70	hbint 3225	. . . . . . . . . . . . . . . . . . 19 |- (x e. |^|{a e. On | (A` a) =/= (B` a)} -> A.a x e. |^|{a e. On | (A` a) =/= (B` a)})
72		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> A.a x e. On)
73		ax-17 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. A -> A.a x e. A)
74	73, 71	hbfv 4686	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (A` |^|{a e. On | (A` a) =/= (B` a)}) -> A.a x e. (A` |^|{a e. On | (A` a) =/= (B` a)}))
75		ax-17 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. B -> A.a x e. B)
76	75, 71	hbfv 4686	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (B` |^|{a e. On | (A` a) =/= (B` a)}) -> A.a x e. (B` |^|{a e. On | (A` a) =/= (B` a)}))
77	74, 76	hbne 2103	. . . . . . . . . . . . . . . . . . 19 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)}) -> A.a(A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)}))
78		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (a = |^|{a e. On | (A` a) =/= (B` a)} -> (A` a) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
79		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (a = |^|{a e. On | (A` a) =/= (B` a)} -> (B` a) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
80	78, 79	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . 20 |- (a = |^|{a e. On | (A` a) =/= (B` a)} -> ((A` a) = (B` a) <-> (A` |^|{a e. On | (A` a) =/= (B` a)}) = (B` |^|{a e. On | (A` a) =/= (B` a)})))
81	80	necon3bid 2035	. . . . . . . . . . . . . . . . . . 19 |- (a = |^|{a e. On | (A` a) =/= (B` a)} -> ((A` a) =/= (B` a) <-> (A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)})))
82	71, 72, 77, 81	elrabf 2413	. . . . . . . . . . . . . . . . . 18 |- (|^|{a e. On | (A` a) =/= (B` a)} e. {a e. On | (A` a) =/= (B` a)} <-> (|^|{a e. On | (A` a) =/= (B` a)} e. On /\ (A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)})))
83	82	simprbi 353	. . . . . . . . . . . . . . . . 17 |- (|^|{a e. On | (A` a) =/= (B` a)} e. {a e. On | (A` a) =/= (B` a)} -> (A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)}))
84	69, 83	syl 12	. . . . . . . . . . . . . . . 16 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> (A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)}))
85		df-ne 2019	. . . . . . . . . . . . . . . 16 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) =/= (B` |^|{a e. On | (A` a) =/= (B` a)}) <-> -. (A` |^|{a e. On | (A` a) =/= (B` a)}) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
86	84, 85	sylib 215	. . . . . . . . . . . . . . 15 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> -. (A` |^|{a e. On | (A` a) =/= (B` a)}) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
87		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (y = |^|{a e. On | (A` a) =/= (B` a)} -> (A` y) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
88		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (y = |^|{a e. On | (A` a) =/= (B` a)} -> (B` y) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
89	87, 88	eqeq12d 1899	. . . . . . . . . . . . . . . . 17 |- (y = |^|{a e. On | (A` a) =/= (B` a)} -> ((A` y) = (B` y) <-> (A` |^|{a e. On | (A` a) =/= (B` a)}) = (B` |^|{a e. On | (A` a) =/= (B` a)})))
90	89	rcla4cv 2377	. . . . . . . . . . . . . . . 16 |- (A.y e. x (A` y) = (B` y) -> (|^|{a e. On | (A` a) =/= (B` a)} e. x -> (A` |^|{a e. On | (A` a) =/= (B` a)}) = (B` |^|{a e. On | (A` a) =/= (B` a)})))
91	90	ad2antlr 441	. . . . . . . . . . . . . . 15 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> (|^|{a e. On | (A` a) =/= (B` a)} e. x -> (A` |^|{a e. On | (A` a) =/= (B` a)}) = (B` |^|{a e. On | (A` a) =/= (B` a)})))
92	86, 91	mtod 123	. . . . . . . . . . . . . 14 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> -. |^|{a e. On | (A` a) =/= (B` a)} e. x)
93		simpll 448	. . . . . . . . . . . . . . 15 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> x e. On)
94		oninton 3881	. . . . . . . . . . . . . . . . 17 |- (({a e. On | (A` a) =/= (B` a)} C_ On /\ {a e. On | (A` a) =/= (B` a)} =/= (/)) -> |^|{a e. On | (A` a) =/= (B` a)} e. On)
95	94, 66, 67	sylancr 526	. . . . . . . . . . . . . . . 16 |- (x e. {a e. On | (A` a) =/= (B` a)} -> |^|{a e. On | (A` a) =/= (B` a)} e. On)
96	95	adantl 424	. . . . . . . . . . . . . . 15 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> |^|{a e. On | (A` a) =/= (B` a)} e. On)
97		ontri1 3695	. . . . . . . . . . . . . . 15 |- ((x e. On /\ |^|{a e. On | (A` a) =/= (B` a)} e. On) -> (x C_ |^|{a e. On | (A` a) =/= (B` a)} <-> -. |^|{a e. On | (A` a) =/= (B` a)} e. x))
98	93, 96, 97	syl11anc 524	. . . . . . . . . . . . . 14 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> (x C_ |^|{a e. On | (A` a) =/= (B` a)} <-> -. |^|{a e. On | (A` a) =/= (B` a)} e. x))
99	92, 98	mpbird 213	. . . . . . . . . . . . 13 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> x C_ |^|{a e. On | (A` a) =/= (B` a)})
100		intss1 3231	. . . . . . . . . . . . . 14 |- (x e. {a e. On | (A` a) =/= (B` a)} -> |^|{a e. On | (A` a) =/= (B` a)} C_ x)
101	100	adantl 424	. . . . . . . . . . . . 13 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> |^|{a e. On | (A` a) =/= (B` a)} C_ x)
102	99, 101	eqssd 2633	. . . . . . . . . . . 12 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> x = |^|{a e. On | (A` a) =/= (B` a)})
103	64, 102	syldan 516	. . . . . . . . . . 11 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x) =/= (B` x)) -> x = |^|{a e. On | (A` a) =/= (B` a)})
104		eqeq12 1896	. . . . . . . . . . . . . 14 |- (((A` x) = 1o /\ (B` x) = (/)) -> ((A` x) = (B` x) <-> 1o = (/)))
105	10, 104	mtbiri 785	. . . . . . . . . . . . 13 |- (((A` x) = 1o /\ (B` x) = (/)) -> -. (A` x) = (B` x))
106		1on 5182	. . . . . . . . . . . . . . . . 17 |- 1o e. On
107		0elon 3716	. . . . . . . . . . . . . . . . 17 |- (/) e. On
108		suc11 3773	. . . . . . . . . . . . . . . . . 18 |- ((1o e. On /\ (/) e. On) -> (suc 1o = suc (/) <-> 1o = (/)))
109	108	necon3bid 2035	. . . . . . . . . . . . . . . . 17 |- ((1o e. On /\ (/) e. On) -> (suc 1o =/= suc (/) <-> 1o =/= (/)))
110	106, 107, 109	mp2an 761	. . . . . . . . . . . . . . . 16 |- (suc 1o =/= suc (/) <-> 1o =/= (/))
111	8, 110	mpbir 207	. . . . . . . . . . . . . . 15 |- suc 1o =/= suc (/)
112		df-2o 5178	. . . . . . . . . . . . . . . 16 |- 2o = suc 1o
113		df-1o 5177	. . . . . . . . . . . . . . . 16 |- 1o = suc (/)
114	112, 113	eqeq12i 1897	. . . . . . . . . . . . . . 15 |- (2o = 1o <-> suc 1o = suc (/))
115	111, 114	nemtbir 2099	. . . . . . . . . . . . . 14 |- -. 2o = 1o
116		eqeq12 1896	. . . . . . . . . . . . . . 15 |- (((A` x) = 1o /\ (B` x) = 2o) -> ((A` x) = (B` x) <-> 1o = 2o))
117		eqcom 1886	. . . . . . . . . . . . . . 15 |- (1o = 2o <-> 2o = 1o)
118	116, 117	syl6bb 595	. . . . . . . . . . . . . 14 |- (((A` x) = 1o /\ (B` x) = 2o) -> ((A` x) = (B` x) <-> 2o = 1o))
119	115, 118	mtbiri 785	. . . . . . . . . . . . 13 |- (((A` x) = 1o /\ (B` x) = 2o) -> -. (A` x) = (B` x))
120		eqcom 1886	. . . . . . . . . . . . . . 15 |- (2o = (/) <-> (/) = 2o)
121	19, 120	mtbi 208	. . . . . . . . . . . . . 14 |- -. (/) = 2o
122		eqeq12 1896	. . . . . . . . . . . . . 14 |- (((A` x) = (/) /\ (B` x) = 2o) -> ((A` x) = (B` x) <-> (/) = 2o))
123	121, 122	mtbiri 785	. . . . . . . . . . . . 13 |- (((A` x) = (/) /\ (B` x) = 2o) -> -. (A` x) = (B` x))
124	105, 119, 123	3jaoi 1160	. . . . . . . . . . . 12 |- ((((A` x) = 1o /\ (B` x) = (/)) \/ ((A` x) = 1o /\ (B` x) = 2o) \/ ((A` x) = (/) /\ (B` x) = 2o)) -> -. (A` x) = (B` x))
125		fvex 4689	. . . . . . . . . . . . 13 |- (A` x) e. _V
126		fvex 4689	. . . . . . . . . . . . 13 |- (B` x) e. _V
127	125, 126, 4, 6, 6	brtp 13830	. . . . . . . . . . . 12 |- ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) <-> (((A` x) = 1o /\ (B` x) = (/)) \/ ((A` x) = 1o /\ (B` x) = 2o) \/ ((A` x) = (/) /\ (B` x) = 2o)))
128		df-ne 2019	. . . . . . . . . . . 12 |- ((A` x) =/= (B` x) <-> -. (A` x) = (B` x))
129	124, 127, 128	3imtr4i 236	. . . . . . . . . . 11 |- ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) -> (A` x) =/= (B` x))
130	103, 129	sylan2 500	. . . . . . . . . 10 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> x = |^|{a e. On | (A` a) =/= (B` a)})
131	130	fveq2d 4685	. . . . . . . . 9 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> (A` x) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
132	130	fveq2d 4685	. . . . . . . . 9 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> (B` x) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
133	131, 132	breq12d 3351	. . . . . . . 8 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) <-> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
134	133	biimpd 170	. . . . . . 7 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) -> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
135	134	ex 402	. . . . . 6 |- ((x e. On /\ A.y e. x (A` y) = (B` y)) -> ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) -> ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) -> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))))
136	135	pm2.43d 79	. . . . 5 |- ((x e. On /\ A.y e. x (A` y) = (B` y)) -> ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) -> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
137	136	expimpd 404	. . . 4 |- (x e. On -> ((A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)})))
138	137	r19.23aiv 2211	. . 3 |- (E.x e. On (A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x)) -> (A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}))
139	57, 138	impbid1 575	. 2 |- ((A e. No /\ B e. No ) -> ((A` |^|{a e. On | (A` a) =/= (B` a)}){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` |^|{a e. On | (A` a) =/= (B` a)}) <-> E.x e. On (A.y e. x (A` y) = (B` y) /\ (A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x))))
140	1, 139	bitr4d 590	1 |- ((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)})))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  <.cop 3046  {ctp 3051  |^|cint 3214   class class class wbr 3338  Oncon0 3657  suc csuc 3659  ` cfv 3998  1oc1o 5172  2oc2o 5173   No csur 13981   <s cslt 13982

This theorem is referenced by:  sltsgn1 14002  sltsgn2 14003  sltintdifex 14004  axdenselem8 14026  axfelem12 14042

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-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-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-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-suc 3663  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-1o 5177  df-2o 5178  df-slt 13985

Copyright terms: Public domain