Theorem frfi 15771

Description: A partial order is founded on a finite set.

Assertion

Ref	Expression
frfi	|- ((R Po A /\ A e. Fin) -> R Fr A)

Proof of Theorem frfi

Step	Hyp	Ref	Expression
1		poeq2 3595	. . . 4 |- (x = (/) -> (R Po x <-> R Po (/)))
2		freq2 3633	. . . 4 |- (x = (/) -> (R Fr x <-> R Fr (/)))
3	1, 2	imbi12d 688	. . 3 |- (x = (/) -> ((R Po x -> R Fr x) <-> (R Po (/) -> R Fr (/))))
4		poeq2 3595	. . . 4 |- (x = (y \ {z}) -> (R Po x <-> R Po (y \ {z})))
5		freq2 3633	. . . 4 |- (x = (y \ {z}) -> (R Fr x <-> R Fr (y \ {z})))
6	4, 5	imbi12d 688	. . 3 |- (x = (y \ {z}) -> ((R Po x -> R Fr x) <-> (R Po (y \ {z}) -> R Fr (y \ {z}))))
7		poeq2 3595	. . . 4 |- (x = y -> (R Po x <-> R Po y))
8		freq2 3633	. . . 4 |- (x = y -> (R Fr x <-> R Fr y))
9	7, 8	imbi12d 688	. . 3 |- (x = y -> ((R Po x -> R Fr x) <-> (R Po y -> R Fr y)))
10		poeq2 3595	. . . 4 |- (x = A -> (R Po x <-> R Po A))
11		freq2 3633	. . . 4 |- (x = A -> (R Fr x <-> R Fr A))
12	10, 11	imbi12d 688	. . 3 |- (x = A -> ((R Po x -> R Fr x) <-> (R Po A -> R Fr A)))
13		fr0 3636	. . . 4 |- R Fr (/)
14	13	a1i 8	. . 3 |- (R Po (/) -> R Fr (/))
15		ssel2 2616	. . . . . . . . . . . . . . 15 |- ((x C_ y /\ w e. x) -> w e. y)
16		sneq 3054	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> {z} = {w})
17	16	difeq2d 2726	. . . . . . . . . . . . . . . . . 18 |- (z = w -> (y \ {z}) = (y \ {w}))
18		poeq2 3595	. . . . . . . . . . . . . . . . . 18 |- ((y \ {z}) = (y \ {w}) -> (R Po (y \ {z}) <-> R Po (y \ {w})))
19	17, 18	syl 12	. . . . . . . . . . . . . . . . 17 |- (z = w -> (R Po (y \ {z}) <-> R Po (y \ {w})))
20		freq2 3633	. . . . . . . . . . . . . . . . . 18 |- ((y \ {z}) = (y \ {w}) -> (R Fr (y \ {z}) <-> R Fr (y \ {w})))
21	17, 20	syl 12	. . . . . . . . . . . . . . . . 17 |- (z = w -> (R Fr (y \ {z}) <-> R Fr (y \ {w})))
22	19, 21	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (z = w -> ((R Po (y \ {z}) -> R Fr (y \ {z})) <-> (R Po (y \ {w}) -> R Fr (y \ {w}))))
23	22	rcla4v 2376	. . . . . . . . . . . . . . 15 |- (w e. y -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> (R Po (y \ {w}) -> R Fr (y \ {w}))))
24	15, 23	syl 12	. . . . . . . . . . . . . 14 |- ((x C_ y /\ w e. x) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> (R Po (y \ {w}) -> R Fr (y \ {w}))))
25	24	adantll 428	. . . . . . . . . . . . 13 |- ((((R Po y /\ y e. Fin) /\ x C_ y) /\ w e. x) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> (R Po (y \ {w}) -> R Fr (y \ {w}))))
26		difss 2735	. . . . . . . . . . . . . . . . . 18 |- (y \ {w}) C_ y
27		poss 3592	. . . . . . . . . . . . . . . . . 18 |- ((y \ {w}) C_ y -> (R Po y -> R Po (y \ {w})))
28	26, 27	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (R Po y -> R Po (y \ {w}))
29		pm2.27 76	. . . . . . . . . . . . . . . . 17 |- (R Po (y \ {w}) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (y \ {w})))
30	28, 29	syl 12	. . . . . . . . . . . . . . . 16 |- (R Po y -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (y \ {w})))
31		ssdif 2740	. . . . . . . . . . . . . . . . 17 |- (x C_ y -> (x \ {w}) C_ (y \ {w}))
32		frss 3630	. . . . . . . . . . . . . . . . 17 |- ((x \ {w}) C_ (y \ {w}) -> (R Fr (y \ {w}) -> R Fr (x \ {w})))
33	31, 32	syl 12	. . . . . . . . . . . . . . . 16 |- (x C_ y -> (R Fr (y \ {w}) -> R Fr (x \ {w})))
34	30, 33	sylan9 517	. . . . . . . . . . . . . . 15 |- ((R Po y /\ x C_ y) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (x \ {w})))
35	34	adantlr 429	. . . . . . . . . . . . . 14 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (x \ {w})))
36	35	adantr 425	. . . . . . . . . . . . 13 |- ((((R Po y /\ y e. Fin) /\ x C_ y) /\ w e. x) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (x \ {w})))
37		eqss 2631	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = {w} <-> (x C_ {w} /\ {w} C_ x))
38	37	biimpri 169	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x C_ {w} /\ {w} C_ x) -> x = {w})
39		ssdif0 2934	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x C_ {w} <-> (x \ {w}) = (/))
40	39	biimpri 169	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x \ {w}) = (/) -> x C_ {w})
41		snssi 3129	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. x -> {w} C_ x)
42	38, 40, 41	syl2an 503	. . . . . . . . . . . . . . . . . . . . 21 |- (((x \ {w}) = (/) /\ w e. x) -> x = {w})
43	42	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (w e. x -> ((x \ {w}) = (/) -> x = {w}))
44	43	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((R Po x /\ w e. x) -> ((x \ {w}) = (/) -> x = {w}))
45		simplr 449	. . . . . . . . . . . . . . . . . . . . 21 |- (((R Po x /\ w e. x) /\ x = {w}) -> w e. x)
46		raleq 2266	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = {w} -> (A.v e. x -. vRw <-> A.v e. {w} -. vRw))
47		poirr 3597	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R Po x /\ w e. x) -> -. wRw)
48		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- w e. _V
49	48	ralsn 3084	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.v e. {w} -. vRw <-> [w / v] -. vRw)
50		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v = w -> (vRw <-> wRw))
51	50	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = w -> (-. vRw <-> -. wRw))
52	48, 51	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ([w / v] -. vRw <-> -. wRw)
53	49, 52	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.v e. {w} -. vRw <-> -. wRw)
54	47, 53	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R Po x /\ w e. x) -> A.v e. {w} -. vRw)
55	46, 54	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R Po x /\ w e. x) -> (x = {w} -> A.v e. x -. vRw))
56	55	imp 377	. . . . . . . . . . . . . . . . . . . . 21 |- (((R Po x /\ w e. x) /\ x = {w}) -> A.v e. x -. vRw)
57		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = w -> (vRu <-> vRw))
58	57	notbid 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u = w -> (-. vRu <-> -. vRw))
59	58	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = w -> (A.v e. x -. vRu <-> A.v e. x -. vRw))
60	59	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. x /\ A.v e. x -. vRw) -> E.u e. x A.v e. x -. vRu)
61	45, 56, 60	syl11anc 524	. . . . . . . . . . . . . . . . . . . 20 |- (((R Po x /\ w e. x) /\ x = {w}) -> E.u e. x A.v e. x -. vRu)
62	61	ex 402	. . . . . . . . . . . . . . . . . . 19 |- ((R Po x /\ w e. x) -> (x = {w} -> E.u e. x A.v e. x -. vRu))
63	44, 62	syld 30	. . . . . . . . . . . . . . . . . 18 |- ((R Po x /\ w e. x) -> ((x \ {w}) = (/) -> E.u e. x A.v e. x -. vRu))
64	63	a1dd 53	. . . . . . . . . . . . . . . . 17 |- ((R Po x /\ w e. x) -> ((x \ {w}) = (/) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu)))
65		simpllr 453	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> w e. x)
66	47	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> -. wRw)
67	66, 53	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. {w} -. vRw)
68		potr 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((R Po x /\ (z e. x /\ w e. x /\ y e. x)) -> ((zRw /\ wRy) -> zRy))
69	68	3exp2 1086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (R Po x -> (z e. x -> (w e. x -> (y e. x -> ((zRw /\ wRy) -> zRy)))))
70	69	com34 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (R Po x -> (z e. x -> (y e. x -> (w e. x -> ((zRw /\ wRy) -> zRy)))))
71	70	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (R Po x -> (w e. x -> (y e. x -> (z e. x -> ((zRw /\ wRy) -> zRy)))))
72	71	imp41 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((R Po x /\ w e. x) /\ y e. x) /\ z e. x) -> ((zRw /\ wRy) -> zRy))
73	72	ancomsd 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((R Po x /\ w e. x) /\ y e. x) /\ z e. x) -> ((wRy /\ zRw) -> zRy))
74	73	expdimp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((R Po x /\ w e. x) /\ y e. x) /\ z e. x) /\ wRy) -> (zRw -> zRy))
75	74	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((R Po x /\ w e. x) /\ y e. x) /\ wRy) /\ z e. x) -> (zRw -> zRy))
76		eldifi 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z e. (x \ {w}) -> z e. x)
77	75, 76	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((R Po x /\ w e. x) /\ y e. x) /\ wRy) /\ z e. (x \ {w})) -> (zRw -> zRy))
78	77	con3d 111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((R Po x /\ w e. x) /\ y e. x) /\ wRy) /\ z e. (x \ {w})) -> (-. zRy -> -. zRw))
79	78	ralimdvaa 2171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((R Po x /\ w e. x) /\ y e. x) /\ wRy) -> (A.z e. (x \ {w}) -. zRy -> A.z e. (x \ {w}) -. zRw))
80	79	anasss 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((R Po x /\ w e. x) /\ (y e. x /\ wRy)) -> (A.z e. (x \ {w}) -. zRy -> A.z e. (x \ {w}) -. zRw))
81		eldifi 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y e. (x \ {w}) -> y e. x)
82	80, 81	sylanr1 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) -> (A.z e. (x \ {w}) -. zRy -> A.z e. (x \ {w}) -. zRw))
83	82	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.z e. (x \ {w}) -. zRw)
84		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = v -> (zRw <-> vRw))
85	84	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (z = v -> (-. zRw <-> -. vRw))
86	85	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.z e. (x \ {w}) -. zRw <-> A.v e. (x \ {w}) -. vRw)
87	83, 86	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. (x \ {w}) -. vRw)
88		ralun 2785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A.v e. {w} -. vRw /\ A.v e. (x \ {w}) -. vRw) -> A.v e. ({w} u. (x \ {w})) -. vRw)
89	67, 87, 88	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. ({w} u. (x \ {w})) -. vRw)
90		undif 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ({w} C_ x <-> ({w} u. (x \ {w})) = x)
91	41, 90	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. x -> ({w} u. (x \ {w})) = x)
92	91	raleqdv 2269	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. x -> (A.v e. ({w} u. (x \ {w})) -. vRw <-> A.v e. x -. vRw))
93	92	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((R Po x /\ w e. x) -> (A.v e. ({w} u. (x \ {w})) -. vRw <-> A.v e. x -. vRw))
94	93	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> (A.v e. ({w} u. (x \ {w})) -. vRw <-> A.v e. x -. vRw))
95	89, 94	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. x -. vRw)
96	65, 95, 60	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> E.u e. x A.v e. x -. vRu)
97	96	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) -> (A.z e. (x \ {w}) -. zRy -> E.u e. x A.v e. x -. vRu))
98	97	expr 418	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (wRy -> (A.z e. (x \ {w}) -. zRy -> E.u e. x A.v e. x -. vRu)))
99	91	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> ({w} u. (x \ {w})) = x)
100	99	raleqdv 2269	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (A.z e. ({w} u. (x \ {w})) -. zRy <-> A.z e. x -. zRy))
101		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u = y -> (vRu <-> vRy))
102	101	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (u = y -> (-. vRu <-> -. vRy))
103	102	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (u = y -> (A.v e. x -. vRu <-> A.v e. x -. vRy))
104		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = z -> (vRy <-> zRy))
105	104	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (v = z -> (-. vRy <-> -. zRy))
106	105	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.v e. x -. vRy <-> A.z e. x -. zRy)
107	103, 106	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (u = y -> (A.v e. x -. vRu <-> A.z e. x -. zRy))
108	107	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. x /\ A.z e. x -. zRy) -> E.u e. x A.v e. x -. vRu)
109	108	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. x -> (A.z e. x -. zRy -> E.u e. x A.v e. x -. vRu))
110	81, 109	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. (x \ {w}) -> (A.z e. x -. zRy -> E.u e. x A.v e. x -. vRu))
111	110	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (A.z e. x -. zRy -> E.u e. x A.v e. x -. vRu))
112	100, 111	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (A.z e. ({w} u. (x \ {w})) -. zRy -> E.u e. x A.v e. x -. vRu))
113		ralun 2785	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.z e. {w} -. zRy /\ A.z e. (x \ {w}) -. zRy) -> A.z e. ({w} u. (x \ {w})) -. zRy)
114	112, 113	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> ((A.z e. {w} -. zRy /\ A.z e. (x \ {w}) -. zRy) -> E.u e. x A.v e. x -. vRu))
115	114	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (A.z e. {w} -. zRy -> (A.z e. (x \ {w}) -. zRy -> E.u e. x A.v e. x -. vRu)))
116	48	ralsn 3084	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.z e. {w} -. zRy <-> [w / z] -. zRy)
117		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = w -> (zRy <-> wRy))
118	117	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = w -> (-. zRy <-> -. wRy))
119	48, 118	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ([w / z] -. zRy <-> -. wRy)
120	116, 119	bitri 190	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.z e. {w} -. zRy <-> -. wRy)
121	115, 120	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (-. wRy -> (A.z e. (x \ {w}) -. zRy -> E.u e. x A.v e. x -. vRu)))
122	98, 121	pm2.61d 141	. . . . . . . . . . . . . . . . . . . . 21 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (A.z e. (x \ {w}) -. zRy -> E.u e. x A.v e. x -. vRu))
123	122	r19.23adva 2216	. . . . . . . . . . . . . . . . . . . 20 |- ((R Po x /\ w e. x) -> (E.y e. (x \ {w})A.z e. (x \ {w}) -. zRy -> E.u e. x A.v e. x -. vRu))
124		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- x e. _V
125		difexg 3458	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. _V -> (x \ {w}) e. _V)
126	124, 125	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- (x \ {w}) e. _V
127		ssid 2634	. . . . . . . . . . . . . . . . . . . . . 22 |- (x \ {w}) C_ (x \ {w})
128		fri 3626	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((x \ {w}) e. _V /\ R Fr (x \ {w})) /\ ((x \ {w}) C_ (x \ {w}) /\ (x \ {w}) =/= (/))) -> E.y e. (x \ {w})A.z e. (x \ {w}) -. zRy)
129	127, 128	mpanr1 774	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x \ {w}) e. _V /\ R Fr (x \ {w})) /\ (x \ {w}) =/= (/)) -> E.y e. (x \ {w})A.z e. (x \ {w}) -. zRy)
130	126, 129	mpanl1 770	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr (x \ {w}) /\ (x \ {w}) =/= (/)) -> E.y e. (x \ {w})A.z e. (x \ {w}) -. zRy)
131	123, 130	syl5 20	. . . . . . . . . . . . . . . . . . 19 |- ((R Po x /\ w e. x) -> ((R Fr (x \ {w}) /\ (x \ {w}) =/= (/)) -> E.u e. x A.v e. x -. vRu))
132	131	exp3a 405	. . . . . . . . . . . . . . . . . 18 |- ((R Po x /\ w e. x) -> (R Fr (x \ {w}) -> ((x \ {w}) =/= (/) -> E.u e. x A.v e. x -. vRu)))
133	132	com23 36	. . . . . . . . . . . . . . . . 17 |- ((R Po x /\ w e. x) -> ((x \ {w}) =/= (/) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu)))
134	64, 133	pm2.61dne 2091	. . . . . . . . . . . . . . . 16 |- ((R Po x /\ w e. x) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu))
135	134	adantlr 429	. . . . . . . . . . . . . . 15 |- (((R Po x /\ x e. Fin) /\ w e. x) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu))
136	135	adantlr 429	. . . . . . . . . . . . . 14 |- ((((R Po x /\ x e. Fin) /\ x C_ y) /\ w e. x) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu))
137		poss 3592	. . . . . . . . . . . . . . . 16 |- (x C_ y -> (R Po y -> R Po x))
138		ssfi 5630	. . . . . . . . . . . . . . . . 17 |- ((y e. Fin /\ x C_ y) -> x e. Fin)
139	138	expcom 403	. . . . . . . . . . . . . . . 16 |- (x C_ y -> (y e. Fin -> x e. Fin))
140	137, 139	anim12d 617	. . . . . . . . . . . . . . 15 |- (x C_ y -> ((R Po y /\ y e. Fin) -> (R Po x /\ x e. Fin)))
141	140	imdistanri 492	. . . . . . . . . . . . . 14 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> ((R Po x /\ x e. Fin) /\ x C_ y))
142	136, 141	sylan 497	. . . . . . . . . . . . 13 |- ((((R Po y /\ y e. Fin) /\ x C_ y) /\ w e. x) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu))
143	25, 36, 142	3syld 31	. . . . . . . . . . . 12 |- ((((R Po y /\ y e. Fin) /\ x C_ y) /\ w e. x) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> E.u e. x A.v e. x -. vRu))
144	143	ex 402	. . . . . . . . . . 11 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> (w e. x -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> E.u e. x A.v e. x -. vRu)))
145	144	19.23adv 1584	. . . . . . . . . 10 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> (E.w w e. x -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> E.u e. x A.v e. x -. vRu)))
146		n0 2884	. . . . . . . . . 10 |- (x =/= (/) <-> E.w w e. x)
147	145, 146	syl5ib 223	. . . . . . . . 9 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> (x =/= (/) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> E.u e. x A.v e. x -. vRu)))
148	147	expimpd 404	. . . . . . . 8 |- ((R Po y /\ y e. Fin) -> ((x C_ y /\ x =/= (/)) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> E.u e. x A.v e. x -. vRu)))
149	148	com23 36	. . . . . . 7 |- ((R Po y /\ y e. Fin) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> ((x C_ y /\ x =/= (/)) -> E.u e. x A.v e. x -. vRu)))
150	149	19.21adv 1666	. . . . . 6 |- ((R Po y /\ y e. Fin) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> A.x((x C_ y /\ x =/= (/)) -> E.u e. x A.v e. x -. vRu)))
151		df-fr 3625	. . . . . 6 |- (R Fr y <-> A.x((x C_ y /\ x =/= (/)) -> E.u e. x A.v e. x -. vRu))
152	150, 151	syl6ibr 230	. . . . 5 |- ((R Po y /\ y e. Fin) -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> R Fr y))
153	152	expcom 403	. . . 4 |- (y e. Fin -> (R Po y -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> R Fr y)))
154	153	com23 36	. . 3 |- (y e. Fin -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> (R Po y -> R Fr y)))
155	3, 6, 9, 12, 14, 154	findcard 10178	. 2 |- (A e. Fin -> (R Po A -> R Fr A))
156	155	impcom 378	1 |- ((R Po A /\ A e. Fin) -> R Fr A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   u. cun 2591   C_ wss 2593  (/)c0 2875  {csn 3044   class class class wbr 3338   Po wpo 3589   Fr wfr 3623  Fincfn 5426

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-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