Theorem fimax 15746

Description: A finite set has a maximum under a total order.

Hypothesis

Ref	Expression
fimax.1	|- R Or A

Assertion

Ref	Expression
fimax	|- ((A e. Fin /\ A =/= (/)) -> E.x e. A A.y e. A (x =/= y -> yRx))

Distinct variable groups:   x,A,y   x,R,y

Proof of Theorem fimax

Step	Hyp	Ref	Expression
1		ssid 2634	. 2 |- A C_ A
2		neeq1 2024	. . . . 5 |- (z = (/) -> (z =/= (/) <-> (/) =/= (/)))
3		sseq1 2637	. . . . . 6 |- (z = (/) -> (z C_ A <-> (/) C_ A))
4		raleq 2266	. . . . . . 7 |- (z = (/) -> (A.y e. z (x =/= y -> yRx) <-> A.y e. (/) (x =/= y -> yRx)))
5	4	rexeqbi1dv 2272	. . . . . 6 |- (z = (/) -> (E.x e. z A.y e. z (x =/= y -> yRx) <-> E.x e. (/) A.y e. (/) (x =/= y -> yRx)))
6	3, 5	imbi12d 688	. . . . 5 |- (z = (/) -> ((z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx)) <-> ((/) C_ A -> E.x e. (/) A.y e. (/) (x =/= y -> yRx))))
7	2, 6	imbi12d 688	. . . 4 |- (z = (/) -> ((z =/= (/) -> (z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx))) <-> ((/) =/= (/) -> ((/) C_ A -> E.x e. (/) A.y e. (/) (x =/= y -> yRx)))))
8		neeq1 2024	. . . . 5 |- (z = (w \ {u}) -> (z =/= (/) <-> (w \ {u}) =/= (/)))
9		sseq1 2637	. . . . . 6 |- (z = (w \ {u}) -> (z C_ A <-> (w \ {u}) C_ A))
10		raleq 2266	. . . . . . 7 |- (z = (w \ {u}) -> (A.y e. z (x =/= y -> yRx) <-> A.y e. (w \ {u})(x =/= y -> yRx)))
11	10	rexeqbi1dv 2272	. . . . . 6 |- (z = (w \ {u}) -> (E.x e. z A.y e. z (x =/= y -> yRx) <-> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx)))
12	9, 11	imbi12d 688	. . . . 5 |- (z = (w \ {u}) -> ((z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx)) <-> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))))
13	8, 12	imbi12d 688	. . . 4 |- (z = (w \ {u}) -> ((z =/= (/) -> (z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx))) <-> ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx)))))
14		neeq1 2024	. . . . 5 |- (z = w -> (z =/= (/) <-> w =/= (/)))
15		sseq1 2637	. . . . . 6 |- (z = w -> (z C_ A <-> w C_ A))
16		raleq 2266	. . . . . . 7 |- (z = w -> (A.y e. z (x =/= y -> yRx) <-> A.y e. w (x =/= y -> yRx)))
17	16	rexeqbi1dv 2272	. . . . . 6 |- (z = w -> (E.x e. z A.y e. z (x =/= y -> yRx) <-> E.x e. w A.y e. w (x =/= y -> yRx)))
18	15, 17	imbi12d 688	. . . . 5 |- (z = w -> ((z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx)) <-> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx))))
19	14, 18	imbi12d 688	. . . 4 |- (z = w -> ((z =/= (/) -> (z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx))) <-> (w =/= (/) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
20		neeq1 2024	. . . . 5 |- (z = A -> (z =/= (/) <-> A =/= (/)))
21		sseq1 2637	. . . . . 6 |- (z = A -> (z C_ A <-> A C_ A))
22		raleq 2266	. . . . . . 7 |- (z = A -> (A.y e. z (x =/= y -> yRx) <-> A.y e. A (x =/= y -> yRx)))
23	22	rexeqbi1dv 2272	. . . . . 6 |- (z = A -> (E.x e. z A.y e. z (x =/= y -> yRx) <-> E.x e. A A.y e. A (x =/= y -> yRx)))
24	21, 23	imbi12d 688	. . . . 5 |- (z = A -> ((z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx)) <-> (A C_ A -> E.x e. A A.y e. A (x =/= y -> yRx))))
25	20, 24	imbi12d 688	. . . 4 |- (z = A -> ((z =/= (/) -> (z C_ A -> E.x e. z A.y e. z (x =/= y -> yRx))) <-> (A =/= (/) -> (A C_ A -> E.x e. A A.y e. A (x =/= y -> yRx)))))
26		eqid 1884	. . . . . 6 |- (/) = (/)
27		df-ne 2019	. . . . . . 7 |- ((/) =/= (/) <-> -. (/) = (/))
28	27	con2bii 238	. . . . . 6 |- ((/) = (/) <-> -. (/) =/= (/))
29	26, 28	mpbi 206	. . . . 5 |- -. (/) =/= (/)
30	29	pm2.21i 93	. . . 4 |- ((/) =/= (/) -> ((/) C_ A -> E.x e. (/) A.y e. (/) (x =/= y -> yRx)))
31		equid 1484	. . . . . . . . . . 11 |- v = v
32		eleq2 1958	. . . . . . . . . . . 12 |- (w = {v} -> (v e. w <-> v e. {v}))
33		visset 2295	. . . . . . . . . . . . 13 |- v e. _V
34	33	elsnc 3065	. . . . . . . . . . . 12 |- (v e. {v} <-> v = v)
35	32, 34	syl6bb 595	. . . . . . . . . . 11 |- (w = {v} -> (v e. w <-> v = v))
36	31, 35	mpbiri 211	. . . . . . . . . 10 |- (w = {v} -> v e. w)
37		eleq2 1958	. . . . . . . . . . . . 13 |- (w = {v} -> (y e. w <-> y e. {v}))
38		elsn 3058	. . . . . . . . . . . . 13 |- (y e. {v} <-> y = v)
39	37, 38	syl6bb 595	. . . . . . . . . . . 12 |- (w = {v} -> (y e. w <-> y = v))
40		equcom 1488	. . . . . . . . . . . . . 14 |- (y = v <-> v = y)
41		df-ne 2019	. . . . . . . . . . . . . . 15 |- (v =/= y <-> -. v = y)
42	41	con2bii 238	. . . . . . . . . . . . . 14 |- (v = y <-> -. v =/= y)
43	40, 42	bitri 190	. . . . . . . . . . . . 13 |- (y = v <-> -. v =/= y)
44		pm2.21 92	. . . . . . . . . . . . 13 |- (-. v =/= y -> (v =/= y -> yRv))
45	43, 44	sylbi 216	. . . . . . . . . . . 12 |- (y = v -> (v =/= y -> yRv))
46	39, 45	syl6bi 231	. . . . . . . . . . 11 |- (w = {v} -> (y e. w -> (v =/= y -> yRv)))
47	46	r19.21aiv 2175	. . . . . . . . . 10 |- (w = {v} -> A.y e. w (v =/= y -> yRv))
48		neeq1 2024	. . . . . . . . . . . . 13 |- (x = v -> (x =/= y <-> v =/= y))
49		breq2 3342	. . . . . . . . . . . . 13 |- (x = v -> (yRx <-> yRv))
50	48, 49	imbi12d 688	. . . . . . . . . . . 12 |- (x = v -> ((x =/= y -> yRx) <-> (v =/= y -> yRv)))
51	50	ralbidv 2123	. . . . . . . . . . 11 |- (x = v -> (A.y e. w (x =/= y -> yRx) <-> A.y e. w (v =/= y -> yRv)))
52	51	rcla4ev 2381	. . . . . . . . . 10 |- ((v e. w /\ A.y e. w (v =/= y -> yRv)) -> E.x e. w A.y e. w (x =/= y -> yRx))
53	36, 47, 52	syl11anc 524	. . . . . . . . 9 |- (w = {v} -> E.x e. w A.y e. w (x =/= y -> yRx))
54	53	19.23aiv 1674	. . . . . . . 8 |- (E.v w = {v} -> E.x e. w A.y e. w (x =/= y -> yRx))
55	54	a1d 15	. . . . . . 7 |- (E.v w = {v} -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))
56	55	a1d 15	. . . . . 6 |- (E.v w = {v} -> ((w e. Fin /\ A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) /\ w =/= (/)) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx))))
57	56	3expd 1085	. . . . 5 |- (E.v w = {v} -> (w e. Fin -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (w =/= (/) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx))))))
58		n0 2884	. . . . . . . 8 |- (w =/= (/) <-> E.t t e. w)
59		sneq 3054	. . . . . . . . . . . . . 14 |- (u = t -> {u} = {t})
60	59	difeq2d 2726	. . . . . . . . . . . . 13 |- (u = t -> (w \ {u}) = (w \ {t}))
61	60	neeq1d 2028	. . . . . . . . . . . 12 |- (u = t -> ((w \ {u}) =/= (/) <-> (w \ {t}) =/= (/)))
62	60	sseq1d 2644	. . . . . . . . . . . . 13 |- (u = t -> ((w \ {u}) C_ A <-> (w \ {t}) C_ A))
63	60	raleqdv 2269	. . . . . . . . . . . . . 14 |- (u = t -> (A.y e. (w \ {u})(x =/= y -> yRx) <-> A.y e. (w \ {t})(x =/= y -> yRx)))
64	60, 63	rexeqbidv 2275	. . . . . . . . . . . . 13 |- (u = t -> (E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx) <-> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)))
65	62, 64	imbi12d 688	. . . . . . . . . . . 12 |- (u = t -> (((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx)) <-> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))))
66	61, 65	imbi12d 688	. . . . . . . . . . 11 |- (u = t -> (((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) <-> ((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)))))
67	66	rcla4v 2376	. . . . . . . . . 10 |- (t e. w -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> ((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)))))
68		visset 2295	. . . . . . . . . . . . . . 15 |- t e. _V
69	68	snss 3122	. . . . . . . . . . . . . 14 |- (t e. w <-> {t} C_ w)
70		pssdifn0 2936	. . . . . . . . . . . . . . 15 |- (({t} C_ w /\ {t} =/= w) -> (w \ {t}) =/= (/))
71	70	ex 402	. . . . . . . . . . . . . 14 |- ({t} C_ w -> ({t} =/= w -> (w \ {t}) =/= (/)))
72	69, 71	sylbi 216	. . . . . . . . . . . . 13 |- (t e. w -> ({t} =/= w -> (w \ {t}) =/= (/)))
73		sneq 3054	. . . . . . . . . . . . . . . . 17 |- (v = t -> {v} = {t})
74	73	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (v = t -> (w = {v} <-> w = {t}))
75	68, 74	cla4ev 2371	. . . . . . . . . . . . . . 15 |- (w = {t} -> E.v w = {v})
76	75	eqcoms 1887	. . . . . . . . . . . . . 14 |- ({t} = w -> E.v w = {v})
77	76	necon3bi 2045	. . . . . . . . . . . . 13 |- (-. E.v w = {v} -> {t} =/= w)
78	72, 77	syl5 20	. . . . . . . . . . . 12 |- (t e. w -> (-. E.v w = {v} -> (w \ {t}) =/= (/)))
79		pm2.27 76	. . . . . . . . . . . . . 14 |- ((w \ {t}) =/= (/) -> (((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))))
80		ssdifss 2736	. . . . . . . . . . . . . . . 16 |- (w C_ A -> (w \ {t}) C_ A)
81		pm2.27 76	. . . . . . . . . . . . . . . . . 18 |- ((w \ {t}) C_ A -> (((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)) -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)))
82		neeq1 2024	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = s -> (x =/= y <-> s =/= y))
83		breq2 3342	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = s -> (yRx <-> yRs))
84	82, 83	imbi12d 688	. . . . . . . . . . . . . . . . . . . . 21 |- (x = s -> ((x =/= y -> yRx) <-> (s =/= y -> yRs)))
85	84	ralbidv 2123	. . . . . . . . . . . . . . . . . . . 20 |- (x = s -> (A.y e. (w \ {t})(x =/= y -> yRx) <-> A.y e. (w \ {t})(s =/= y -> yRs)))
86	85	cbvrexv 2281	. . . . . . . . . . . . . . . . . . 19 |- (E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx) <-> E.s e. (w \ {t})A.y e. (w \ {t})(s =/= y -> yRs))
87		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w C_ A -> (t e. w -> t e. A))
88	80	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w C_ A -> (s e. (w \ {t}) -> s e. A))
89	87, 88	anim12d 617	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w C_ A -> ((t e. w /\ s e. (w \ {t})) -> (t e. A /\ s e. A)))
90		fimax.1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- R Or A
91		sotrieq 3616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((R Or A /\ (t e. A /\ s e. A)) -> (t = s <-> -. (tRs \/ sRt)))
92	90, 91	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. A /\ s e. A) -> (t = s <-> -. (tRs \/ sRt)))
93		eldifn 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (s e. (w \ {t}) -> -. s e. {t})
94		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (s e. {t} <-> s = t)
95		equcom 1488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (s = t <-> t = s)
96	94, 95	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (s e. {t} <-> t = s)
97	96	notbii 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (-. s e. {t} <-> -. t = s)
98	93, 97	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (s e. (w \ {t}) -> -. t = s)
99		con2bi 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((t = s <-> -. (tRs \/ sRt)) <-> ((tRs \/ sRt) <-> -. t = s))
100	99	biimpi 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((t = s <-> -. (tRs \/ sRt)) -> ((tRs \/ sRt) <-> -. t = s))
101		eldifi 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (s e. (w \ {t}) -> s e. w)
102	101	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((tRs /\ s e. (w \ {t}) /\ t e. w) -> s e. w)
103	102	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> s e. w)
104		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (u = t -> (uRs <-> tRs))
105	104	biimprcd 173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (tRs -> (u = t -> uRs))
106	105	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (tRs -> (u = t -> (s =/= u -> uRs)))
107	106	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (tRs -> (u = t -> (u e. w -> (s =/= u -> uRs))))
108	107	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((tRs /\ s e. (w \ {t}) /\ t e. w) -> (u = t -> (u e. w -> (s =/= u -> uRs))))
109	108	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (u = t -> (u e. w -> (s =/= u -> uRs))))
110	109	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u = t -> (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (u e. w -> (s =/= u -> uRs))))
111		eldifsn 3123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (u e. (w \ {t}) <-> (u e. w /\ u =/= t))
112		neeq2 2025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (y = u -> (s =/= y <-> s =/= u))
113		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (y = u -> (yRs <-> uRs))
114	112, 113	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y = u -> ((s =/= y -> yRs) <-> (s =/= u -> uRs)))
115	114	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (A.y e. (w \ {t})(s =/= y -> yRs) -> (u e. (w \ {t}) -> (s =/= u -> uRs)))
116	115	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (u e. (w \ {t}) -> (s =/= u -> uRs)))
117	116	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (u e. (w \ {t}) -> (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (s =/= u -> uRs)))
118	111, 117	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((u e. w /\ u =/= t) -> (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (s =/= u -> uRs)))
119	118	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (u e. w -> (u =/= t -> (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (s =/= u -> uRs))))
120	119	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u =/= t -> (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (u e. w -> (s =/= u -> uRs))))
121	110, 120	pm2.61ine 2089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> (u e. w -> (s =/= u -> uRs)))
122	121	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> A.u e. w (s =/= u -> uRs))
123		neeq2 2025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u = y -> (s =/= u <-> s =/= y))
124		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u = y -> (uRs <-> yRs))
125	123, 124	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (u = y -> ((s =/= u -> uRs) <-> (s =/= y -> yRs)))
126	125	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.u e. w (s =/= u -> uRs) <-> A.y e. w (s =/= y -> yRs))
127	122, 126	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> A.y e. w (s =/= y -> yRs))
128	84	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = s -> (A.y e. w (x =/= y -> yRx) <-> A.y e. w (s =/= y -> yRs)))
129	128	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((s e. w /\ A.y e. w (s =/= y -> yRs)) -> E.x e. w A.y e. w (x =/= y -> yRx))
130	103, 127, 129	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((tRs /\ s e. (w \ {t}) /\ t e. w) /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs)) -> E.x e. w A.y e. w (x =/= y -> yRx))
131	130	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((tRs /\ s e. (w \ {t}) /\ t e. w) -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))
132	131	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (tRs -> (s e. (w \ {t}) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))))
133		simpr1 882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> t e. w)
134	114	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (u e. (w \ {t}) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> (s =/= u -> uRs)))
135		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (s = u -> (sRt <-> uRt))
136	135	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((s = u /\ sRt) -> uRt)
137	136	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((s = u /\ (sRt /\ s e. (w \ {t}))) -> uRt)
138	137	3ad2antr1 1041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((s = u /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> uRt)
139	138	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (s = u -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt))
140	139	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (s = u -> ((s =/= u -> uRs) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt)))
141	140	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (s = u -> (u e. (w \ {t}) -> ((s =/= u -> uRs) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt))))
142		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (s =/= u -> ((s =/= u -> uRs) -> uRs))
143		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> uRs)
144		simp31l 999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> sRt)
145		sotr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((R Or A /\ (u e. A /\ s e. A /\ t e. A)) -> ((uRs /\ sRt) -> uRt))
146	80	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (w C_ A -> (u e. (w \ {t}) -> u e. A))
147	146	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((u e. (w \ {t}) /\ w C_ A) -> u e. A)
148	147	3ad2antr3 1043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> u e. A)
149	148	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> u e. A)
150	88	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((s e. (w \ {t}) /\ w C_ A) -> s e. A)
151	150	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (((sRt /\ s e. (w \ {t})) /\ w C_ A) -> s e. A)
152	151	3adant2 895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> s e. A)
153	152	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> s e. A)
154	87	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((t e. w /\ w C_ A) -> t e. A)
155	154	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> t e. A)
156	155	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> t e. A)
157	149, 153, 156	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> (u e. A /\ s e. A /\ t e. A))
158	145, 90, 157	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> ((uRs /\ sRt) -> uRt))
159	143, 144, 158	mp2and 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((uRs /\ u e. (w \ {t}) /\ ((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A)) -> uRt)
160	159	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (uRs -> (u e. (w \ {t}) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt)))
161	142, 160	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (s =/= u -> ((s =/= u -> uRs) -> (u e. (w \ {t}) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt))))
162	161	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (s =/= u -> (u e. (w \ {t}) -> ((s =/= u -> uRs) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt))))
163	141, 162	pm2.61ine 2089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (u e. (w \ {t}) -> ((s =/= u -> uRs) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt)))
164	134, 163	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (u e. (w \ {t}) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> uRt)))
165	164	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((sRt /\ s e. (w \ {t})) /\ t e. w /\ w C_ A) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> (u e. (w \ {t}) -> uRt)))
166	165	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((sRt /\ s e. (w \ {t})) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> (u e. (w \ {t}) -> uRt)))))
167	166	3imp2 1083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> (u e. (w \ {t}) -> uRt))
168		necom 2094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (u =/= t <-> t =/= u)
169	168	anbi2i 538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((u e. w /\ u =/= t) <-> (u e. w /\ t =/= u))
170	111, 169	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (u e. (w \ {t}) <-> (u e. w /\ t =/= u))
171	167, 170	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> ((u e. w /\ t =/= u) -> uRt))
172	171	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> (u e. w -> (t =/= u -> uRt)))
173	172	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> A.u e. w (t =/= u -> uRt))
174		neeq2 2025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u = y -> (t =/= u <-> t =/= y))
175		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u = y -> (uRt <-> yRt))
176	174, 175	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (u = y -> ((t =/= u -> uRt) <-> (t =/= y -> yRt)))
177	176	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.u e. w (t =/= u -> uRt) <-> A.y e. w (t =/= y -> yRt))
178	173, 177	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> A.y e. w (t =/= y -> yRt))
179		neeq1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = t -> (x =/= y <-> t =/= y))
180		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = t -> (yRx <-> yRt))
181	179, 180	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = t -> ((x =/= y -> yRx) <-> (t =/= y -> yRt)))
182	181	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = t -> (A.y e. w (x =/= y -> yRx) <-> A.y e. w (t =/= y -> yRt)))
183	182	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((t e. w /\ A.y e. w (t =/= y -> yRt)) -> E.x e. w A.y e. w (x =/= y -> yRx))
184	133, 178, 183	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((sRt /\ s e. (w \ {t})) /\ (t e. w /\ w C_ A /\ A.y e. (w \ {t})(s =/= y -> yRs))) -> E.x e. w A.y e. w (x =/= y -> yRx))
185	184	3exp2 1086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((sRt /\ s e. (w \ {t})) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))
186	185	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (sRt -> (s e. (w \ {t}) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))))
187	132, 186	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((tRs \/ sRt) -> (s e. (w \ {t}) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))))
188	100, 187	syl6bir 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((t = s <-> -. (tRs \/ sRt)) -> (-. t = s -> (s e. (w \ {t}) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))))
189	188	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (s e. (w \ {t}) -> (-. t = s -> ((t = s <-> -. (tRs \/ sRt)) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))))
190	98, 189	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (s e. (w \ {t}) -> ((t = s <-> -. (tRs \/ sRt)) -> (t e. w -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))))
191	190	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t = s <-> -. (tRs \/ sRt)) -> (t e. w -> (s e. (w \ {t}) -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))))
192	191	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t = s <-> -. (tRs \/ sRt)) -> ((t e. w /\ s e. (w \ {t})) -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))
193	92, 192	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. A /\ s e. A) -> ((t e. w /\ s e. (w \ {t})) -> (w C_ A -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))
194	193	com13 37	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w C_ A -> ((t e. w /\ s e. (w \ {t})) -> ((t e. A /\ s e. A) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))
195	89, 194	mpdd 57	. . . . . . . . . . . . . . . . . . . . . 22 |- (w C_ A -> ((t e. w /\ s e. (w \ {t})) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx))))
196	195	exp3a 405	. . . . . . . . . . . . . . . . . . . . 21 |- (w C_ A -> (t e. w -> (s e. (w \ {t}) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> E.x e. w A.y e. w (x =/= y -> yRx)))))
197	196	com4t 44	. . . . . . . . . . . . . . . . . . . 20 |- (s e. (w \ {t}) -> (A.y e. (w \ {t})(s =/= y -> yRs) -> (w C_ A -> (t e. w -> E.x e. w A.y e. w (x =/= y -> yRx)))))
198	197	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . 19 |- (E.s e. (w \ {t})A.y e. (w \ {t})(s =/= y -> yRs) -> (w C_ A -> (t e. w -> E.x e. w A.y e. w (x =/= y -> yRx))))
199	86, 198	sylbi 216	. . . . . . . . . . . . . . . . . 18 |- (E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx) -> (w C_ A -> (t e. w -> E.x e. w A.y e. w (x =/= y -> yRx))))
200	81, 199	syl6 25	. . . . . . . . . . . . . . . . 17 |- ((w \ {t}) C_ A -> (((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)) -> (w C_ A -> (t e. w -> E.x e. w A.y e. w (x =/= y -> yRx)))))
201	200	com3r 39	. . . . . . . . . . . . . . . 16 |- (w C_ A -> ((w \ {t}) C_ A -> (((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)) -> (t e. w -> E.x e. w A.y e. w (x =/= y -> yRx)))))
202	80, 201	mpd 29	. . . . . . . . . . . . . . 15 |- (w C_ A -> (((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)) -> (t e. w -> E.x e. w A.y e. w (x =/= y -> yRx))))
203	202	com3l 38	. . . . . . . . . . . . . 14 |- (((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx)) -> (t e. w -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx))))
204	79, 203	syl6 25	. . . . . . . . . . . . 13 |- ((w \ {t}) =/= (/) -> (((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))) -> (t e. w -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
205	204	com3r 39	. . . . . . . . . . . 12 |- (t e. w -> ((w \ {t}) =/= (/) -> (((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
206	78, 205	syld 30	. . . . . . . . . . 11 |- (t e. w -> (-. E.v w = {v} -> (((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
207	206	com23 36	. . . . . . . . . 10 |- (t e. w -> (((w \ {t}) =/= (/) -> ((w \ {t}) C_ A -> E.x e. (w \ {t})A.y e. (w \ {t})(x =/= y -> yRx))) -> (-. E.v w = {v} -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
208	67, 207	syld 30	. . . . . . . . 9 |- (t e. w -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (-. E.v w = {v} -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
209	208	19.23aiv 1674	. . . . . . . 8 |- (E.t t e. w -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (-. E.v w = {v} -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
210	58, 209	sylbi 216	. . . . . . 7 |- (w =/= (/) -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (-. E.v w = {v} -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
211	210	com13 37	. . . . . 6 |- (-. E.v w = {v} -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (w =/= (/) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
212	211	a1d 15	. . . . 5 |- (-. E.v w = {v} -> (w e. Fin -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (w =/= (/) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx))))))
213	57, 212	pm2.61i 140	. . . 4 |- (w e. Fin -> (A.u e. w ((w \ {u}) =/= (/) -> ((w \ {u}) C_ A -> E.x e. (w \ {u})A.y e. (w \ {u})(x =/= y -> yRx))) -> (w =/= (/) -> (w C_ A -> E.x e. w A.y e. w (x =/= y -> yRx)))))
214	7, 13, 19, 25, 30, 213	findcard 10178	. . 3 |- (A e. Fin -> (A =/= (/) -> (A C_ A -> E.x e. A A.y e. A (x =/= y -> yRx))))
215	214	imp 377	. 2 |- ((A e. Fin /\ A =/= (/)) -> (A C_ A -> E.x e. A A.y e. A (x =/= y -> yRx)))
216	1, 215	mpi 55	1 |- ((A e. Fin /\ A =/= (/)) -> E.x e. A A.y e. A (x =/= y -> yRx))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106   \ cdif 2590   C_ wss 2593  (/)c0 2875  {csn 3044   class class class wbr 3338   Or wor 3590  Fincfn 5426

This theorem is referenced by:  fimaxg 15747  totbndbnd 15944

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-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-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-om 3950  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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-1o 5177  df-er 5318  df-en 5427  df-fin 5430

Copyright terms: Public domain