Theorem frfi 5895

Description: A partial order is founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010.)

Assertion

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

Proof of Theorem frfi

Step	Hyp	Ref	Expression
1		poeq2 3787	. . . 4 |- (x = (/) -> (R Po x <-> R Po (/)))
2		freq2 3820	. . . 4 |- (x = (/) -> (R Fr x <-> R Fr (/)))
3	1, 2	imbi12d 384	. . 3 |- (x = (/) -> ((R Po x -> R Fr x) <-> (R Po (/) -> R Fr (/))))
4		poeq2 3787	. . . 4 |- (x = (y \ {z}) -> (R Po x <-> R Po (y \ {z})))
5		freq2 3820	. . . 4 |- (x = (y \ {z}) -> (R Fr x <-> R Fr (y \ {z})))
6	4, 5	imbi12d 384	. . 3 |- (x = (y \ {z}) -> ((R Po x -> R Fr x) <-> (R Po (y \ {z}) -> R Fr (y \ {z}))))
7		poeq2 3787	. . . 4 |- (x = y -> (R Po x <-> R Po y))
8		freq2 3820	. . . 4 |- (x = y -> (R Fr x <-> R Fr y))
9	7, 8	imbi12d 384	. . 3 |- (x = y -> ((R Po x -> R Fr x) <-> (R Po y -> R Fr y)))
10		poeq2 3787	. . . 4 |- (x = A -> (R Po x <-> R Po A))
11		freq2 3820	. . . 4 |- (x = A -> (R Fr x <-> R Fr A))
12	10, 11	imbi12d 384	. . 3 |- (x = A -> ((R Po x -> R Fr x) <-> (R Po A -> R Fr A)))
13		fr0 3823	. . . 4 |- R Fr (/)
14	13	a1i 8	. . 3 |- (R Po (/) -> R Fr (/))
15		n0 3123	. . . . . . . . . 10 |- (x =/= (/) <-> E.w w e. x)
16		ssel2 2879	. . . . . . . . . . . . . . 15 |- ((x C_ y /\ w e. x) -> w e. y)
17		sneq 3279	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> {z} = {w})
18	17	difeq2d 2978	. . . . . . . . . . . . . . . . . 18 |- (z = w -> (y \ {z}) = (y \ {w}))
19		poeq2 3787	. . . . . . . . . . . . . . . . . 18 |- ((y \ {z}) = (y \ {w}) -> (R Po (y \ {z}) <-> R Po (y \ {w})))
20	18, 19	syl 13	. . . . . . . . . . . . . . . . 17 |- (z = w -> (R Po (y \ {z}) <-> R Po (y \ {w})))
21		freq2 3820	. . . . . . . . . . . . . . . . . 18 |- ((y \ {z}) = (y \ {w}) -> (R Fr (y \ {z}) <-> R Fr (y \ {w})))
22	18, 21	syl 13	. . . . . . . . . . . . . . . . 17 |- (z = w -> (R Fr (y \ {z}) <-> R Fr (y \ {w})))
23	20, 22	imbi12d 384	. . . . . . . . . . . . . . . 16 |- (z = w -> ((R Po (y \ {z}) -> R Fr (y \ {z})) <-> (R Po (y \ {w}) -> R Fr (y \ {w}))))
24	23	rcla4v 2647	. . . . . . . . . . . . . . 15 |- (w e. y -> (A.z e. y (R Po (y \ {z}) -> R Fr (y \ {z})) -> (R Po (y \ {w}) -> R Fr (y \ {w}))))
25	16, 24	syl 13	. . . . . . . . . . . . . 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}))))
26	25	adantll 832	. . . . . . . . . . . . 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}))))
27		difss 2986	. . . . . . . . . . . . . . . . . 18 |- (y \ {w}) C_ y
28		poss 3785	. . . . . . . . . . . . . . . . . 18 |- ((y \ {w}) C_ y -> (R Po y -> R Po (y \ {w})))
29	27, 28	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (R Po y -> R Po (y \ {w}))
30		pm2.27 67	. . . . . . . . . . . . . . . . 17 |- (R Po (y \ {w}) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (y \ {w})))
31	29, 30	syl 13	. . . . . . . . . . . . . . . 16 |- (R Po y -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (y \ {w})))
32		ssdif 2991	. . . . . . . . . . . . . . . . 17 |- (x C_ y -> (x \ {w}) C_ (y \ {w}))
33		frss 3818	. . . . . . . . . . . . . . . . 17 |- ((x \ {w}) C_ (y \ {w}) -> (R Fr (y \ {w}) -> R Fr (x \ {w})))
34	32, 33	syl 13	. . . . . . . . . . . . . . . 16 |- (x C_ y -> (R Fr (y \ {w}) -> R Fr (x \ {w})))
35	31, 34	sylan9 751	. . . . . . . . . . . . . . 15 |- ((R Po y /\ x C_ y) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (x \ {w})))
36	35	adantlr 834	. . . . . . . . . . . . . 14 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> ((R Po (y \ {w}) -> R Fr (y \ {w})) -> R Fr (x \ {w})))
37	36	adantr 543	. . . . . . . . . . . . 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})))
38		poss 3785	. . . . . . . . . . . . . . . 16 |- (x C_ y -> (R Po y -> R Po x))
39		ssfi 5880	. . . . . . . . . . . . . . . . 17 |- ((y e. Fin /\ x C_ y) -> x e. Fin)
40	39	expcom 495	. . . . . . . . . . . . . . . 16 |- (x C_ y -> (y e. Fin -> x e. Fin))
41	38, 40	anim12d 629	. . . . . . . . . . . . . . 15 |- (x C_ y -> ((R Po y /\ y e. Fin) -> (R Po x /\ x e. Fin)))
42	41	imdistanri 828	. . . . . . . . . . . . . 14 |- (((R Po y /\ y e. Fin) /\ x C_ y) -> ((R Po x /\ x e. Fin) /\ x C_ y))
43		ssdif0 3167	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x C_ {w} <-> (x \ {w}) = (/))
44	43	biimpri 243	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x \ {w}) = (/) -> x C_ {w})
45		snssi 3354	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. x -> {w} C_ x)
46		eqss 2892	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = {w} <-> (x C_ {w} /\ {w} C_ x))
47	46	biimpri 243	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x C_ {w} /\ {w} C_ x) -> x = {w})
48	44, 45, 47	syl2an 699	. . . . . . . . . . . . . . . . . . . . 21 |- (((x \ {w}) = (/) /\ w e. x) -> x = {w})
49	48	expcom 495	. . . . . . . . . . . . . . . . . . . 20 |- (w e. x -> ((x \ {w}) = (/) -> x = {w}))
50	49	adantl 544	. . . . . . . . . . . . . . . . . . 19 |- ((R Po x /\ w e. x) -> ((x \ {w}) = (/) -> x = {w}))
51		simplr 868	. . . . . . . . . . . . . . . . . . . . 21 |- (((R Po x /\ w e. x) /\ x = {w}) -> w e. x)
52		poirr 3789	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R Po x /\ w e. x) -> -. wRw)
53		visset 2572	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- w e. _V
54	53	ralsn 3307	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.v e. {w} -. vRw <-> [w / v] -. vRw)
55		breq1 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v = w -> (vRw <-> wRw))
56	55	notbid 356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = w -> (-. vRw <-> -. wRw))
57	53, 56	sbcie 2755	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ([w / v] -. vRw <-> -. wRw)
58	54, 57	bitri 306	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.v e. {w} -. vRw <-> -. wRw)
59	52, 58	sylibr 264	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R Po x /\ w e. x) -> A.v e. {w} -. vRw)
60		raleq 2542	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = {w} -> (A.v e. x -. vRw <-> A.v e. {w} -. vRw))
61	59, 60	syl5ibrcom 279	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R Po x /\ w e. x) -> (x = {w} -> A.v e. x -. vRw))
62	61	imp 489	. . . . . . . . . . . . . . . . . . . . 21 |- (((R Po x /\ w e. x) /\ x = {w}) -> A.v e. x -. vRw)
63		breq2 3543	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = w -> (vRu <-> vRw))
64	63	notbid 356	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u = w -> (-. vRu <-> -. vRw))
65	64	ralbidv 2403	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = w -> (A.v e. x -. vRu <-> A.v e. x -. vRw))
66	65	rcla4ev 2651	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. x /\ A.v e. x -. vRw) -> E.u e. x A.v e. x -. vRu)
67	51, 62, 66	syl11anc 755	. . . . . . . . . . . . . . . . . . . 20 |- (((R Po x /\ w e. x) /\ x = {w}) -> E.u e. x A.v e. x -. vRu)
68	67	ex 494	. . . . . . . . . . . . . . . . . . 19 |- ((R Po x /\ w e. x) -> (x = {w} -> E.u e. x A.v e. x -. vRu))
69	50, 68	syld 31	. . . . . . . . . . . . . . . . . 18 |- ((R Po x /\ w e. x) -> ((x \ {w}) = (/) -> E.u e. x A.v e. x -. vRu))
70	69	a1dd 97	. . . . . . . . . . . . . . . . 17 |- ((R Po x /\ w e. x) -> ((x \ {w}) = (/) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu)))
71		visset 2572	. . . . . . . . . . . . . . . . . . . . . 22 |- x e. _V
72		difexg 3657	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. _V -> (x \ {w}) e. _V)
73	71, 72	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- (x \ {w}) e. _V
74		ssid 2895	. . . . . . . . . . . . . . . . . . . . . 22 |- (x \ {w}) C_ (x \ {w})
75		fri 3815	. . . . . . . . . . . . . . . . . . . . . 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)
76	74, 75	mpanr1 792	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x \ {w}) e. _V /\ R Fr (x \ {w})) /\ (x \ {w}) =/= (/)) -> E.y e. (x \ {w})A.z e. (x \ {w}) -. zRy)
77	73, 76	mpanl1 788	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr (x \ {w}) /\ (x \ {w}) =/= (/)) -> E.y e. (x \ {w})A.z e. (x \ {w}) -. zRy)
78		simpllr 872	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> w e. x)
79	52	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> -. wRw)
80	79, 58	sylibr 264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. {w} -. vRw)
81		eldifi 2981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y e. (x \ {w}) -> y e. x)
82		eldifi 2981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z e. (x \ {w}) -> z e. x)
83		potr 3790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((R Po x /\ (z e. x /\ w e. x /\ y e. x)) -> ((zRw /\ wRy) -> zRy))
84	83	3exp2 1363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (R Po x -> (z e. x -> (w e. x -> (y e. x -> ((zRw /\ wRy) -> zRy)))))
85	84	com34 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (R Po x -> (z e. x -> (y e. x -> (w e. x -> ((zRw /\ wRy) -> zRy)))))
86	85	com24 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (R Po x -> (w e. x -> (y e. x -> (z e. x -> ((zRw /\ wRy) -> zRy)))))
87	86	imp41 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((R Po x /\ w e. x) /\ y e. x) /\ z e. x) -> ((zRw /\ wRy) -> zRy))
88	87	ancomsd 513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((R Po x /\ w e. x) /\ y e. x) /\ z e. x) -> ((wRy /\ zRw) -> zRy))
89	88	expdimp 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((R Po x /\ w e. x) /\ y e. x) /\ z e. x) /\ wRy) -> (zRw -> zRy))
90	89	an32s 912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((R Po x /\ w e. x) /\ y e. x) /\ wRy) /\ z e. x) -> (zRw -> zRy))
91	82, 90	sylan2 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((R Po x /\ w e. x) /\ y e. x) /\ wRy) /\ z e. (x \ {w})) -> (zRw -> zRy))
92	91	con3d 157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((R Po x /\ w e. x) /\ y e. x) /\ wRy) /\ z e. (x \ {w})) -> (-. zRy -> -. zRw))
93	92	ralimdva 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((R Po x /\ w e. x) /\ y e. x) /\ wRy) -> (A.z e. (x \ {w}) -. zRy -> A.z e. (x \ {w}) -. zRw))
94	93	anasss 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((R Po x /\ w e. x) /\ (y e. x /\ wRy)) -> (A.z e. (x \ {w}) -. zRy -> A.z e. (x \ {w}) -. zRw))
95	81, 94	sylanr1 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) -> (A.z e. (x \ {w}) -. zRy -> A.z e. (x \ {w}) -. zRw))
96	95	imp 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.z e. (x \ {w}) -. zRw)
97		breq1 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = v -> (zRw <-> vRw))
98	97	notbid 356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (z = v -> (-. zRw <-> -. vRw))
99	98	cbvralv 2557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.z e. (x \ {w}) -. zRw <-> A.v e. (x \ {w}) -. vRw)
100	96, 99	sylib 263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. (x \ {w}) -. vRw)
101		ralun 3030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A.v e. {w} -. vRw /\ A.v e. (x \ {w}) -. vRw) -> A.v e. ({w} u. (x \ {w})) -. vRw)
102	80, 100, 101	syl11anc 755	. . . . . . . . . . . . . . . . . . . . . . . . . 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)
103		undif 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ({w} C_ x <-> ({w} u. (x \ {w})) = x)
104	45, 103	sylib 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. x -> ({w} u. (x \ {w})) = x)
105	104	raleqdv 2546	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. x -> (A.v e. ({w} u. (x \ {w})) -. vRw <-> A.v e. x -. vRw))
106	105	adantl 544	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((R Po x /\ w e. x) -> (A.v e. ({w} u. (x \ {w})) -. vRw <-> A.v e. x -. vRw))
107	106	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . . . . 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))
108	102, 107	mpbid 256	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R Po x /\ w e. x) /\ (y e. (x \ {w}) /\ wRy)) /\ A.z e. (x \ {w}) -. zRy) -> A.v e. x -. vRw)
109	78, 108, 66	syl11anc 755	. . . . . . . . . . . . . . . . . . . . . . . 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)
110	109	ex 494	. . . . . . . . . . . . . . . . . . . . . . 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))
111	110	expr 685	. . . . . . . . . . . . . . . . . . . . . 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)))
112	53	ralsn 3307	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.z e. {w} -. zRy <-> [w / z] -. zRy)
113		breq1 3542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = w -> (zRy <-> wRy))
114	113	notbid 356	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = w -> (-. zRy <-> -. wRy))
115	53, 114	sbcie 2755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ([w / z] -. zRy <-> -. wRy)
116	112, 115	bitri 306	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.z e. {w} -. zRy <-> -. wRy)
117		ralun 3030	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.z e. {w} -. zRy /\ A.z e. (x \ {w}) -. zRy) -> A.z e. ({w} u. (x \ {w})) -. zRy)
118	104	ad2antlr 859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> ({w} u. (x \ {w})) = x)
119	118	raleqdv 2546	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((R Po x /\ w e. x) /\ y e. (x \ {w})) -> (A.z e. ({w} u. (x \ {w})) -. zRy <-> A.z e. x -. zRy))
120		breq2 3543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u = y -> (vRu <-> vRy))
121	120	notbid 356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (u = y -> (-. vRu <-> -. vRy))
122	121	ralbidv 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (u = y -> (A.v e. x -. vRu <-> A.v e. x -. vRy))
123		breq1 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = z -> (vRy <-> zRy))
124	123	notbid 356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (v = z -> (-. vRy <-> -. zRy))
125	124	cbvralv 2557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.v e. x -. vRy <-> A.z e. x -. zRy)
126	122, 125	syl6bb 324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (u = y -> (A.v e. x -. vRu <-> A.z e. x -. zRy))
127	126	rcla4ev 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. x /\ A.z e. x -. zRy) -> E.u e. x A.v e. x -. vRu)
128	127	ex 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. x -> (A.z e. x -. zRy -> E.u e. x A.v e. x -. vRu))
129	81, 128	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. (x \ {w}) -> (A.z e. x -. zRy -> E.u e. x A.v e. x -. vRu))
130	129	adantl 544	. . . . . . . . . . . . . . . . . . . . . . . . . 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))
131	119, 130	sylbid 267	. . . . . . . . . . . . . . . . . . . . . . . . 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))
132	117, 131	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . 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))
133	132	exp3a 496	. . . . . . . . . . . . . . . . . . . . . . 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)))
134	116, 133	syl5bir 272	. . . . . . . . . . . . . . . . . . . . . 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)))
135	111, 134	pm2.61d 203	. . . . . . . . . . . . . . . . . . . . 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))
136	135	r19.23adva 2494	. . . . . . . . . . . . . . . . . . . 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))
137	77, 136	syl5 33	. . . . . . . . . . . . . . . . . . 19 |- ((R Po x /\ w e. x) -> ((R Fr (x \ {w}) /\ (x \ {w}) =/= (/)) -> E.u e. x A.v e. x -. vRu))
138	137	exp3a 496	. . . . . . . . . . . . . . . . . 18 |- ((R Po x /\ w e. x) -> (R Fr (x \ {w}) -> ((x \ {w}) =/= (/) -> E.u e. x A.v e. x -. vRu)))
139	138	com23 68	. . . . . . . . . . . . . . . . 17 |- ((R Po x /\ w e. x) -> ((x \ {w}) =/= (/) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu)))
140	70, 139	pm2.61dne 2369	. . . . . . . . . . . . . . . 16 |- ((R Po x /\ w e. x) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu))
141	140	adantlr 834	. . . . . . . . . . . . . . 15 |- (((R Po x /\ x e. Fin) /\ w e. x) -> (R Fr (x \ {w}) -> E.u e. x A.v e. x -. vRu))
142	141	adantlr 834	. . . . . . . . . . . . . 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))
143	42, 142	sylan 693	. . . . . . . . . . . . 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))
144	26, 37, 143	3syld 54	. . . . . . . . . . . 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))
145	144	ex 494	. . . . . . . . . . 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)))
146	145	19.23adv 1889	. . . . . . . . . 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)))
147	15, 146	syl5bi 270	. . . . . . . . 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 672	. . . . . . . 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 68	. . . . . . 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 1964	. . . . . 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 3814	. . . . . 6 |- (R Fr y <-> A.x((x C_ y /\ x =/= (/)) -> E.u e. x A.v e. x -. vRu))
152	150, 151	syl6ibr 283	. . . . 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 495	. . . 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 68	. . 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 5887	. 2 |- (A e. Fin -> (R Po A -> R Fr A))
156	155	impcom 490	1 |- ((R Po A /\ A e. Fin) -> R Fr A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 231   /\ wa 433  A.wal 1613   = wceq 1615   e. wcel 1617  E.wex 1644  [wsbc 1843   =/= wne 2295  A.wral 2385  E.wrex 2386  _Vcvv 2569   \ cdif 2856   u. cun 2857   C_ wss 2859  (/)c0 3114  {csn 3270   class class class wbr 3539   Po wpo 3782   Fr wfr 3812  Fincfn 5630

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-sbc 2731  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-1o 5384  df-er 5519  df-en 5631  df-fin 5634

Copyright terms: Public domain