Theorem sltval2 14662

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 14654	. 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 4778	. . . . . . . . . . . . 13 |- (A` |^|{a e. On | (A` a) =/= (B` a)}) e. _V
3		fvex 4778	. . . . . . . . . . . . 13 |- (B` |^|{a e. On | (A` a) =/= (B` a)}) e. _V
4		0ex 3614	. . . . . . . . . . . . 13 |- (/) e. _V
5		2on 5350	. . . . . . . . . . . . . 14 |- 2o e. On
6	5	elisseti 2548	. . . . . . . . . . . . 13 |- 2o e. _V
7	2, 3, 4, 6, 6	brtp 14458	. . . . . . . . . . . 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 5353	. . . . . . . . . . . . . . . . 17 |- 1o =/= (/)
9		df-ne 2268	. . . . . . . . . . . . . . . . 17 |- (1o =/= (/) <-> -. 1o = (/))
10	8, 9	mpbi 272	. . . . . . . . . . . . . . . 16 |- -. 1o = (/)
11		eqeq1 2147	. . . . . . . . . . . . . . . 16 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o -> ((A` |^|{a e. On | (A` a) =/= (B` a)}) = (/) <-> 1o = (/)))
12	10, 11	mtbiri 1025	. . . . . . . . . . . . . . 15 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o -> -. (A` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
13		fvprc 4762	. . . . . . . . . . . . . . 15 |- (-. |^|{a e. On | (A` a) =/= (B` a)} e. _V -> (A` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
14	12, 13	nsyl2 168	. . . . . . . . . . . . . 14 |- ((A` |^|{a e. On | (A` a) =/= (B` a)}) = 1o -> |^|{a e. On | (A` a) =/= (B` a)} e. _V)
15	14	adantr 447	. . . . . . . . . . . . 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 447	. . . . . . . . . . . . 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 14494	. . . . . . . . . . . . . . . . 17 |- 2o =/= (/)
18		df-ne 2268	. . . . . . . . . . . . . . . . 17 |- (2o =/= (/) <-> -. 2o = (/))
19	17, 18	mpbi 272	. . . . . . . . . . . . . . . 16 |- -. 2o = (/)
20		eqeq1 2147	. . . . . . . . . . . . . . . 16 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o -> ((B` |^|{a e. On | (A` a) =/= (B` a)}) = (/) <-> 2o = (/)))
21	19, 20	mtbiri 1025	. . . . . . . . . . . . . . 15 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o -> -. (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
22		fvprc 4762	. . . . . . . . . . . . . . 15 |- (-. |^|{a e. On | (A` a) =/= (B` a)} e. _V -> (B` |^|{a e. On | (A` a) =/= (B` a)}) = (/))
23	21, 22	nsyl2 168	. . . . . . . . . . . . . 14 |- ((B` |^|{a e. On | (A` a) =/= (B` a)}) = 2o -> |^|{a e. On | (A` a) =/= (B` a)} e. _V)
24	23	adantl 448	. . . . . . . . . . . . 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 1434	. . . . . . . . . . . 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 225	. . . . . . . . . . 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 4025	. . . . . . . . . . 11 |- (|^|{a e. On | (A` a) =/= (B` a)} e. _V <-> |^|{a e. On | (A` a) =/= (B` a)} e. On)
28	26, 27	sylib 242	. . . . . . . . . 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 448	. . . . . . . . 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 3836	. . . . . . . . . . . . . . 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 399	. . . . . . . . . . . . . 14 |- (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (|^|{a e. On | (A` a) =/= (B` a)} e. On -> y e. On))
32	29, 31	syl5 35	. . . . . . . . . . . . 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 4765	. . . . . . . . . . . . . . . . 17 |- (a = y -> (A` a) = (A` y))
34		fveq2 4765	. . . . . . . . . . . . . . . . 17 |- (a = y -> (B` a) = (B` y))
35	33, 34	eqeq12d 2155	. . . . . . . . . . . . . . . 16 |- (a = y -> ((A` a) = (B` a) <-> (A` y) = (B` y)))
36	35	necon3bid 2300	. . . . . . . . . . . . . . 15 |- (a = y -> ((A` a) =/= (B` a) <-> (A` y) =/= (B` y)))
37	36	onnminsb 4028	. . . . . . . . . . . . . 14 |- (y e. On -> (y e. |^|{a e. On | (A` a) =/= (B` a)} -> -. (A` y) =/= (B` y)))
38	37	com12 26	. . . . . . . . . . . . 13 |- (y e. |^|{a e. On | (A` a) =/= (B` a)} -> (y e. On -> -. (A` y) =/= (B` y)))
39	32, 38	syld 33	. . . . . . . . . . . 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 26	. . . . . . . . . . 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 2268	. . . . . . . . . . . 12 |- ((A` y) =/= (B` y) <-> -. (A` y) = (B` y))
42	41	con2bii 335	. . . . . . . . . . 11 |- ((A` y) = (B` y) <-> -. (A` y) =/= (B` y))
43	40, 42	syl6ibr 262	. . . . . . . . . 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 2425	. . . . . . . . 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 494	. . . . . . . 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 398	. . . . . . 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 593	. . . . . 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 633	. . . . . 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 242	. . . . 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 2511	. . . . . . 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 4765	. . . . . . . 8 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> (A` x) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
52		fveq2 4765	. . . . . . . 8 |- (x = |^|{a e. On | (A` a) =/= (B` a)} -> (B` x) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
53	51, 52	breq12d 3520	. . . . . . 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 763	. . . . . 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 2620	. . . . 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 13	. . . 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 398	. . 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		eqeq12 2153	. . . . . . . . . . . . . 14 |- (((A` x) = 1o /\ (B` x) = (/)) -> ((A` x) = (B` x) <-> 1o = (/)))
59	10, 58	mtbiri 1025	. . . . . . . . . . . . 13 |- (((A` x) = 1o /\ (B` x) = (/)) -> -. (A` x) = (B` x))
60		1on 5349	. . . . . . . . . . . . . . . . 17 |- 1o e. On
61		0elon 3863	. . . . . . . . . . . . . . . . 17 |- (/) e. On
62		suc11 3913	. . . . . . . . . . . . . . . . . 18 |- ((1o e. On /\ (/) e. On) -> (suc 1o = suc (/) <-> 1o = (/)))
63	62	necon3bid 2300	. . . . . . . . . . . . . . . . 17 |- ((1o e. On /\ (/) e. On) -> (suc 1o =/= suc (/) <-> 1o =/= (/)))
64	60, 61, 63	mp2an 681	. . . . . . . . . . . . . . . 16 |- (suc 1o =/= suc (/) <-> 1o =/= (/))
65	8, 64	mpbir 273	. . . . . . . . . . . . . . 15 |- suc 1o =/= suc (/)
66		df-2o 5345	. . . . . . . . . . . . . . . 16 |- 2o = suc 1o
67		df-1o 5344	. . . . . . . . . . . . . . . 16 |- 1o = suc (/)
68	66, 67	eqeq12i 2154	. . . . . . . . . . . . . . 15 |- (2o = 1o <-> suc 1o = suc (/))
69	65, 68	nemtbir 2348	. . . . . . . . . . . . . 14 |- -. 2o = 1o
70		eqeq12 2153	. . . . . . . . . . . . . . 15 |- (((A` x) = 1o /\ (B` x) = 2o) -> ((A` x) = (B` x) <-> 1o = 2o))
71		eqcom 2143	. . . . . . . . . . . . . . 15 |- (1o = 2o <-> 2o = 1o)
72	70, 71	syl6bb 729	. . . . . . . . . . . . . 14 |- (((A` x) = 1o /\ (B` x) = 2o) -> ((A` x) = (B` x) <-> 2o = 1o))
73	69, 72	mtbiri 1025	. . . . . . . . . . . . 13 |- (((A` x) = 1o /\ (B` x) = 2o) -> -. (A` x) = (B` x))
74		eqcom 2143	. . . . . . . . . . . . . . 15 |- (2o = (/) <-> (/) = 2o)
75	19, 74	mtbi 312	. . . . . . . . . . . . . 14 |- -. (/) = 2o
76		eqeq12 2153	. . . . . . . . . . . . . 14 |- (((A` x) = (/) /\ (B` x) = 2o) -> ((A` x) = (B` x) <-> (/) = 2o))
77	75, 76	mtbiri 1025	. . . . . . . . . . . . 13 |- (((A` x) = (/) /\ (B` x) = 2o) -> -. (A` x) = (B` x))
78	59, 73, 77	3jaoi 1434	. . . . . . . . . . . 12 |- ((((A` x) = 1o /\ (B` x) = (/)) \/ ((A` x) = 1o /\ (B` x) = 2o) \/ ((A` x) = (/) /\ (B` x) = 2o)) -> -. (A` x) = (B` x))
79		fvex 4778	. . . . . . . . . . . . 13 |- (A` x) e. _V
80		fvex 4778	. . . . . . . . . . . . 13 |- (B` x) e. _V
81	79, 80, 4, 6, 6	brtp 14458	. . . . . . . . . . . 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)))
82		df-ne 2268	. . . . . . . . . . . 12 |- ((A` x) =/= (B` x) <-> -. (A` x) = (B` x))
83	78, 81, 82	3imtr4i 328	. . . . . . . . . . 11 |- ((A` x){<.1o, (/)>., <.1o, 2o>., <.(/), 2o>.} (B` x) -> (A` x) =/= (B` x))
84		fveq2 4765	. . . . . . . . . . . . . . . . 17 |- (a = x -> (A` a) = (A` x))
85		fveq2 4765	. . . . . . . . . . . . . . . . 17 |- (a = x -> (B` a) = (B` x))
86	84, 85	eqeq12d 2155	. . . . . . . . . . . . . . . 16 |- (a = x -> ((A` a) = (B` a) <-> (A` x) = (B` x)))
87	86	necon3bid 2300	. . . . . . . . . . . . . . 15 |- (a = x -> ((A` a) =/= (B` a) <-> (A` x) =/= (B` x)))
88	87	elrab 2654	. . . . . . . . . . . . . 14 |- (x e. {a e. On | (A` a) =/= (B` a)} <-> (x e. On /\ (A` x) =/= (B` x)))
89	88	biimpri 230	. . . . . . . . . . . . 13 |- ((x e. On /\ (A` x) =/= (B` x)) -> x e. {a e. On | (A` a) =/= (B` a)})
90	89	adantlr 777	. . . . . . . . . . . 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)})
91		ssrab2 2917	. . . . . . . . . . . . . . . . . 18 |- {a e. On | (A` a) =/= (B` a)} C_ On
92		ne0i 3088	. . . . . . . . . . . . . . . . . . 19 |- (x e. {a e. On | (A` a) =/= (B` a)} -> {a e. On | (A` a) =/= (B` a)} =/= (/))
93	92	adantl 448	. . . . . . . . . . . . . . . . . 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)} =/= (/))
94		onint 4019	. . . . . . . . . . . . . . . . . 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)})
95	91, 93, 94	sylancr 662	. . . . . . . . . . . . . . . . 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)})
96		hbrab1 2502	. . . . . . . . . . . . . . . . . . . 20 |- (x e. {a e. On | (A` a) =/= (B` a)} -> A.a x e. {a e. On | (A` a) =/= (B` a)})
97	96	hbint 3410	. . . . . . . . . . . . . . . . . . 19 |- (x e. |^|{a e. On | (A` a) =/= (B` a)} -> A.a x e. |^|{a e. On | (A` a) =/= (B` a)})
98		ax-17 1605	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> A.a x e. On)
99		ax-17 1605	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. A -> A.a x e. A)
100	99, 97	hbfv 4771	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (A` |^|{a e. On | (A` a) =/= (B` a)}) -> A.a x e. (A` |^|{a e. On | (A` a) =/= (B` a)}))
101		ax-17 1605	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. B -> A.a x e. B)
102	101, 97	hbfv 4771	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (B` |^|{a e. On | (A` a) =/= (B` a)}) -> A.a x e. (B` |^|{a e. On | (A` a) =/= (B` a)}))
103	100, 102	hbne 2353	. . . . . . . . . . . . . . . . . . 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)}))
104		fveq2 4765	. . . . . . . . . . . . . . . . . . . . 21 |- (a = |^|{a e. On | (A` a) =/= (B` a)} -> (A` a) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
105		fveq2 4765	. . . . . . . . . . . . . . . . . . . . 21 |- (a = |^|{a e. On | (A` a) =/= (B` a)} -> (B` a) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
106	104, 105	eqeq12d 2155	. . . . . . . . . . . . . . . . . . . 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)})))
107	106	necon3bid 2300	. . . . . . . . . . . . . . . . . . 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)})))
108	97, 98, 103, 107	elrabf 2653	. . . . . . . . . . . . . . . . . 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)})))
109	108	simprbi 446	. . . . . . . . . . . . . . . . 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)}))
110	95, 109	syl 13	. . . . . . . . . . . . . . . 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)}))
111		df-ne 2268	. . . . . . . . . . . . . . . 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)}))
112	110, 111	sylib 242	. . . . . . . . . . . . . . 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)}))
113		fveq2 4765	. . . . . . . . . . . . . . . . . 18 |- (y = |^|{a e. On | (A` a) =/= (B` a)} -> (A` y) = (A` |^|{a e. On | (A` a) =/= (B` a)}))
114		fveq2 4765	. . . . . . . . . . . . . . . . . 18 |- (y = |^|{a e. On | (A` a) =/= (B` a)} -> (B` y) = (B` |^|{a e. On | (A` a) =/= (B` a)}))
115	113, 114	eqeq12d 2155	. . . . . . . . . . . . . . . . 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)})))
116	115	rcla4cv 2617	. . . . . . . . . . . . . . . 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)})))
117	116	ad2antlr 802	. . . . . . . . . . . . . . 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)})))
118	112, 117	mtod 152	. . . . . . . . . . . . . 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)
119		simpll 810	. . . . . . . . . . . . . . 15 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ x e. {a e. On | (A` a) =/= (B` a)}) -> x e. On)
120		oninton 4024	. . . . . . . . . . . . . . . . 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)
121	91, 92, 120	sylancr 662	. . . . . . . . . . . . . . . 16 |- (x e. {a e. On | (A` a) =/= (B` a)} -> |^|{a e. On | (A` a) =/= (B` a)} e. On)
122	121	adantl 448	. . . . . . . . . . . . . . 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)
123		ontri1 3845	. . . . . . . . . . . . . . 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))
124	119, 122, 123	syl11anc 659	. . . . . . . . . . . . . 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))
125	118, 124	mpbird 318	. . . . . . . . . . . . 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)})
126		intss1 3415	. . . . . . . . . . . . . 14 |- (x e. {a e. On | (A` a) =/= (B` a)} -> |^|{a e. On | (A` a) =/= (B` a)} C_ x)
127	126	adantl 448	. . . . . . . . . . . . 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)
128	125, 127	eqssd 2862	. . . . . . . . . . . 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)})
129	90, 128	syldan 595	. . . . . . . . . . 11 |- (((x e. On /\ A.y e. x (A` y) = (B` y)) /\ (A` x) =/= (B` x)) -> x = |^|{a e. On | (A` a) =/= (B` a)})
130	83, 129	sylan2 600	. . . . . . . . . 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 4769	. . . . . . . . 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 4769	. . . . . . . . 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 3520	. . . . . . . 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 231	. . . . . . 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 398	. . . . . 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 109	. . . . 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 576	. . . 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 2459	. . 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 236	. 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 288	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 219   /\ wa 337   \/ w3o 1101   = wceq 1586   e. wcel 1588   =/= wne 2266  A.wral 2355  E.wrex 2356  {crab 2358  _Vcvv 2538   C_ wss 2827  (/)c0 3082  <.cop 3240  {ctp 3244  |^|cint 3400   class class class wbr 3507  Oncon0 3811  suc csuc 3813  ` cfv 4131  1oc1o 5339  2oc2o 5340   No csur 14647   <s cslt 14648

This theorem is referenced by:  sltsgn1 14667  sltsgn2 14668  sltintdifex 14669  sltres 14670  axdenselem8 14695

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-suc 3817  df-xp 4133  df-cnv 4135  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fv 4147  df-1o 5344  df-2o 5345  df-slt 14651

Copyright terms: Public domain