frfi

Description: A partial order is well-founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 29-Jan-2014)

		Ref	Expression
	Assertion	frfi	$⊢ (R Po A \land A \in Fin) \to R Fr A$

Proof

Step	Hyp	Ref	Expression
1		poeq2	$⊢ x = \emptyset \to (R Po x \leftrightarrow R Po \emptyset)$
2		freq2	$⊢ x = \emptyset \to (R Fr x \leftrightarrow R Fr \emptyset)$
3	1 2	imbi12d	$⊢ x = \emptyset \to ((R Po x \to R Fr x) \leftrightarrow (R Po \emptyset \to R Fr \emptyset))$
4		poeq2	$⊢ x = y \to (R Po x \leftrightarrow R Po y)$
5		freq2	$⊢ x = y \to (R Fr x \leftrightarrow R Fr y)$
6	4 5	imbi12d	$⊢ x = y \to ((R Po x \to R Fr x) \leftrightarrow (R Po y \to R Fr y))$
7		poeq2	$⊢ x = y \cup \{w\} \to (R Po x \leftrightarrow R Po (y \cup \{w\}))$
8		freq2	$⊢ x = y \cup \{w\} \to (R Fr x \leftrightarrow R Fr (y \cup \{w\}))$
9	7 8	imbi12d	$⊢ x = y \cup \{w\} \to ((R Po x \to R Fr x) \leftrightarrow (R Po (y \cup \{w\}) \to R Fr (y \cup \{w\})))$
10		poeq2	$⊢ x = A \to (R Po x \leftrightarrow R Po A)$
11		freq2	$⊢ x = A \to (R Fr x \leftrightarrow R Fr A)$
12	10 11	imbi12d	$⊢ x = A \to ((R Po x \to R Fr x) \leftrightarrow (R Po A \to R Fr A))$
13		fr0	$⊢ R Fr \emptyset$
14	13	a1i	$⊢ R Po \emptyset \to R Fr \emptyset$
15		ssun1	$⊢ y \subseteq y \cup \{w\}$
16		poss	$⊢ y \subseteq y \cup \{w\} \to (R Po (y \cup \{w\}) \to R Po y)$
17	15 16	ax-mp	$⊢ R Po (y \cup \{w\}) \to R Po y$
18	17	imim1i	$⊢ (R Po y \to R Fr y) \to (R Po (y \cup \{w\}) \to R Fr y)$
19		uncom	$⊢ y \cup \{w\} = \{w\} \cup y$
20	19	sseq2i	$⊢ x \subseteq y \cup \{w\} \leftrightarrow x \subseteq \{w\} \cup y$
21		ssundif	$⊢ x \subseteq \{w\} \cup y \leftrightarrow x ∖ \{w\} \subseteq y$
22	20 21	bitri	$⊢ x \subseteq y \cup \{w\} \leftrightarrow x ∖ \{w\} \subseteq y$
23	22	anbi1i	$⊢ (x \subseteq y \cup \{w\} \land x \neq \emptyset) \leftrightarrow (x ∖ \{w\} \subseteq y \land x \neq \emptyset)$
24		breq1	$⊢ v = z \to (v R w \leftrightarrow z R w)$
25	24	cbvrexvw	$⊢ \exists v \in x v R w \leftrightarrow \exists z \in x z R w$
26		simpllr	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to R Fr y$
27		simplrl	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to x ∖ \{w\} \subseteq y$
28		poss	$⊢ x \subseteq y \cup \{w\} \to (R Po (y \cup \{w\}) \to R Po x)$
29	28	impcom	$⊢ (R Po (y \cup \{w\}) \land x \subseteq y \cup \{w\}) \to R Po x$
30	22 29	sylan2br	$⊢ (R Po (y \cup \{w\}) \land x ∖ \{w\} \subseteq y) \to R Po x$
31	30	ad2ant2r	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to R Po x$
32		simpr1	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to z \in x$
33		simpr2	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to z R w$
34		poirr	$⊢ (R Po x \land w \in x) \to \neg w R w$
35	34	3ad2antr3	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to \neg w R w$
36		nbrne2	$⊢ (z R w \land \neg w R w) \to z \neq w$
37	33 35 36	syl2anc	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to z \neq w$
38		eldifsn	$⊢ z \in (x ∖ \{w\}) \leftrightarrow (z \in x \land z \neq w)$
39	32 37 38	sylanbrc	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to z \in (x ∖ \{w\})$
40	31 39	sylan	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to z \in (x ∖ \{w\})$
41	40	ne0d	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to x ∖ \{w\} \neq \emptyset$
42		difss	$⊢ x ∖ \{w\} \subseteq x$
43		vex	$⊢ x \in V$
44	43	difexi	$⊢ x ∖ \{w\} \in V$
45		fri	$⊢ ((x ∖ \{w\} \in V \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x ∖ \{w\} \neq \emptyset)) \to \exists u \in (x ∖ \{w\}) \forall v \in (x ∖ \{w\}) \neg v R u$
46	44 45	mpanl1	$⊢ (R Fr y \land (x ∖ \{w\} \subseteq y \land x ∖ \{w\} \neq \emptyset)) \to \exists u \in (x ∖ \{w\}) \forall v \in (x ∖ \{w\}) \neg v R u$
47		ssrexv	$⊢ x ∖ \{w\} \subseteq x \to (\exists u \in (x ∖ \{w\}) \forall v \in (x ∖ \{w\}) \neg v R u \to \exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u)$
48	42 46 47	mpsyl	$⊢ (R Fr y \land (x ∖ \{w\} \subseteq y \land x ∖ \{w\} \neq \emptyset)) \to \exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u$
49	26 27 41 48	syl12anc	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to \exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u$
50		breq1	$⊢ v = z \to (v R u \leftrightarrow z R u)$
51	50	notbid	$⊢ v = z \to (\neg v R u \leftrightarrow \neg z R u)$
52	51	rspcv	$⊢ z \in (x ∖ \{w\}) \to (\forall v \in (x ∖ \{w\}) \neg v R u \to \neg z R u)$
53	39 52	syl	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to (\forall v \in (x ∖ \{w\}) \neg v R u \to \neg z R u)$
54	53	adantr	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\forall v \in (x ∖ \{w\}) \neg v R u \to \neg z R u)$
55		simplr2	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to z R w$
56		simpll	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to R Po x$
57		simplr1	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to z \in x$
58		simplr3	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to w \in x$
59		simpr	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to u \in x$
60		potr	$⊢ (R Po x \land (z \in x \land w \in x \land u \in x)) \to ((z R w \land w R u) \to z R u)$
61	56 57 58 59 60	syl13anc	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to ((z R w \land w R u) \to z R u)$
62	55 61	mpand	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (w R u \to z R u)$
63	62	con3d	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\neg z R u \to \neg w R u)$
64		vex	$⊢ w \in V$
65		breq1	$⊢ v = w \to (v R u \leftrightarrow w R u)$
66	65	notbid	$⊢ v = w \to (\neg v R u \leftrightarrow \neg w R u)$
67	64 66	ralsn	$⊢ \forall v \in \{w\} \neg v R u \leftrightarrow \neg w R u$
68	63 67	syl6ibr	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\neg z R u \to \forall v \in \{w\} \neg v R u)$
69	54 68	syld	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\forall v \in (x ∖ \{w\}) \neg v R u \to \forall v \in \{w\} \neg v R u)$
70		ralun	$⊢ (\forall v \in (x ∖ \{w\}) \neg v R u \land \forall v \in \{w\} \neg v R u) \to \forall v \in ((x ∖ \{w\}) \cup \{w\}) \neg v R u$
71	70	ex	$⊢ \forall v \in (x ∖ \{w\}) \neg v R u \to (\forall v \in \{w\} \neg v R u \to \forall v \in ((x ∖ \{w\}) \cup \{w\}) \neg v R u)$
72	69 71	sylcom	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\forall v \in (x ∖ \{w\}) \neg v R u \to \forall v \in ((x ∖ \{w\}) \cup \{w\}) \neg v R u)$
73		difsnid	$⊢ w \in x \to (x ∖ \{w\}) \cup \{w\} = x$
74	73	raleqdv	$⊢ w \in x \to (\forall v \in ((x ∖ \{w\}) \cup \{w\}) \neg v R u \leftrightarrow \forall v \in x \neg v R u)$
75	58 74	syl	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\forall v \in ((x ∖ \{w\}) \cup \{w\}) \neg v R u \leftrightarrow \forall v \in x \neg v R u)$
76	72 75	sylibd	$⊢ ((R Po x \land (z \in x \land z R w \land w \in x)) \land u \in x) \to (\forall v \in (x ∖ \{w\}) \neg v R u \to \forall v \in x \neg v R u)$
77	76	reximdva	$⊢ (R Po x \land (z \in x \land z R w \land w \in x)) \to (\exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u \to \exists u \in x \forall v \in x \neg v R u)$
78	31 77	sylan	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to (\exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u \to \exists u \in x \forall v \in x \neg v R u)$
79	49 78	mpd	$⊢ (((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \land (z \in x \land z R w \land w \in x)) \to \exists u \in x \forall v \in x \neg v R u$
80	79	3exp2	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to (z \in x \to (z R w \to (w \in x \to \exists u \in x \forall v \in x \neg v R u)))$
81	80	rexlimdv	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to (\exists z \in x z R w \to (w \in x \to \exists u \in x \forall v \in x \neg v R u))$
82	25 81	biimtrid	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to (\exists v \in x v R w \to (w \in x \to \exists u \in x \forall v \in x \neg v R u))$
83		ralnex	$⊢ \forall v \in x \neg v R w \leftrightarrow \neg \exists v \in x v R w$
84		breq2	$⊢ u = w \to (v R u \leftrightarrow v R w)$
85	84	notbid	$⊢ u = w \to (\neg v R u \leftrightarrow \neg v R w)$
86	85	ralbidv	$⊢ u = w \to (\forall v \in x \neg v R u \leftrightarrow \forall v \in x \neg v R w)$
87	86	rspcev	$⊢ (w \in x \land \forall v \in x \neg v R w) \to \exists u \in x \forall v \in x \neg v R u$
88	87	expcom	$⊢ \forall v \in x \neg v R w \to (w \in x \to \exists u \in x \forall v \in x \neg v R u)$
89	83 88	sylbir	$⊢ \neg \exists v \in x v R w \to (w \in x \to \exists u \in x \forall v \in x \neg v R u)$
90	82 89	pm2.61d1	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to (w \in x \to \exists u \in x \forall v \in x \neg v R u)$
91		difsn	$⊢ \neg w \in x \to x ∖ \{w\} = x$
92	48	expr	$⊢ (R Fr y \land x ∖ \{w\} \subseteq y) \to (x ∖ \{w\} \neq \emptyset \to \exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u)$
93		neeq1	$⊢ x ∖ \{w\} = x \to (x ∖ \{w\} \neq \emptyset \leftrightarrow x \neq \emptyset)$
94		raleq	$⊢ x ∖ \{w\} = x \to (\forall v \in (x ∖ \{w\}) \neg v R u \leftrightarrow \forall v \in x \neg v R u)$
95	94	rexbidv	$⊢ x ∖ \{w\} = x \to (\exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u \leftrightarrow \exists u \in x \forall v \in x \neg v R u)$
96	93 95	imbi12d	$⊢ x ∖ \{w\} = x \to ((x ∖ \{w\} \neq \emptyset \to \exists u \in x \forall v \in (x ∖ \{w\}) \neg v R u) \leftrightarrow (x \neq \emptyset \to \exists u \in x \forall v \in x \neg v R u))$
97	92 96	syl5ibcom	$⊢ (R Fr y \land x ∖ \{w\} \subseteq y) \to (x ∖ \{w\} = x \to (x \neq \emptyset \to \exists u \in x \forall v \in x \neg v R u))$
98	97	com23	$⊢ (R Fr y \land x ∖ \{w\} \subseteq y) \to (x \neq \emptyset \to (x ∖ \{w\} = x \to \exists u \in x \forall v \in x \neg v R u))$
99	98	adantll	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land x ∖ \{w\} \subseteq y) \to (x \neq \emptyset \to (x ∖ \{w\} = x \to \exists u \in x \forall v \in x \neg v R u))$
100	99	impr	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to (x ∖ \{w\} = x \to \exists u \in x \forall v \in x \neg v R u)$
101	91 100	syl5	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to (\neg w \in x \to \exists u \in x \forall v \in x \neg v R u)$
102	90 101	pm2.61d	$⊢ ((R Po (y \cup \{w\}) \land R Fr y) \land (x ∖ \{w\} \subseteq y \land x \neq \emptyset)) \to \exists u \in x \forall v \in x \neg v R u$
103	102	ex	$⊢ (R Po (y \cup \{w\}) \land R Fr y) \to ((x ∖ \{w\} \subseteq y \land x \neq \emptyset) \to \exists u \in x \forall v \in x \neg v R u)$
104	23 103	biimtrid	$⊢ (R Po (y \cup \{w\}) \land R Fr y) \to ((x \subseteq y \cup \{w\} \land x \neq \emptyset) \to \exists u \in x \forall v \in x \neg v R u)$
105	104	alrimiv	$⊢ (R Po (y \cup \{w\}) \land R Fr y) \to \forall x ((x \subseteq y \cup \{w\} \land x \neq \emptyset) \to \exists u \in x \forall v \in x \neg v R u)$
106		df-fr	$⊢ R Fr (y \cup \{w\}) \leftrightarrow \forall x ((x \subseteq y \cup \{w\} \land x \neq \emptyset) \to \exists u \in x \forall v \in x \neg v R u)$
107	105 106	sylibr	$⊢ (R Po (y \cup \{w\}) \land R Fr y) \to R Fr (y \cup \{w\})$
108	107	ex	$⊢ R Po (y \cup \{w\}) \to (R Fr y \to R Fr (y \cup \{w\}))$
109	18 108	sylcom	$⊢ (R Po y \to R Fr y) \to (R Po (y \cup \{w\}) \to R Fr (y \cup \{w\}))$
110	109	a1i	$⊢ y \in Fin \to ((R Po y \to R Fr y) \to (R Po (y \cup \{w\}) \to R Fr (y \cup \{w\})))$
111	3 6 9 12 14 110	findcard2	$⊢ A \in Fin \to (R Po A \to R Fr A)$
112	111	impcom	$⊢ (R Po A \land A \in Fin) \to R Fr A$

Metamath Proof Explorer

Theorem frfi

Proof