Theorem frfi 8757

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

Assertion

Ref	Expression
frfi	⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)

Proof of Theorem frfi

Dummy variables 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poeq2 5473	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Po 𝑥 ↔ 𝑅 Po ∅))
2		freq2 5521	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Fr 𝑥 ↔ 𝑅 Fr ∅))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = ∅ → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4		poeq2 5473	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝑦))
5		freq2 5521	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝑦))
6	4, 5	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦 → 𝑅 Fr 𝑦)))
7		poeq2 5473	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥 ↔ 𝑅 Po (𝑦 ∪ {𝑤})))
8		freq2 5521	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥 ↔ 𝑅 Fr (𝑦 ∪ {𝑤})))
9	7, 8	imbi12d 347	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10		poeq2 5473	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝐴))
11		freq2 5521	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝐴))
12	10, 11	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴 → 𝑅 Fr 𝐴)))
13		fr0 5529	. . . 4 ⊢ 𝑅 Fr ∅
14	13	a1i 11	. . 3 ⊢ (𝑅 Po ∅ → 𝑅 Fr ∅)
15		ssun1 4148	. . . . . . 7 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑤})
16		poss 5471	. . . . . . 7 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
17	15, 16	ax-mp 5	. . . . . 6 ⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
18	17	imim1i 63	. . . . 5 ⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19		uncom 4129	. . . . . . . . . . . 12 ⊢ (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
20	19	sseq2i 3996	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21		ssundif 4433	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
22	20, 21	bitri 277	. . . . . . . . . 10 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
23	22	anbi1i 625	. . . . . . . . 9 ⊢ ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅))
24		breq1 5062	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑤 ↔ 𝑧𝑅𝑤))
25	24	cbvrexvw 3451	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 ↔ ∃𝑧 ∈ 𝑥 𝑧𝑅𝑤)
26		simpllr 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑅 Fr 𝑦)
27		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28		poss 5471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
29	28	impcom 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
30	22, 29	sylan2br 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
31	30	ad2ant2r 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32		simpr1 1190	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
33		simpr2 1191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧𝑅𝑤)
34		poirr 5480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ 𝑤 ∈ 𝑥) → ¬ 𝑤𝑅𝑤)
35	34	3ad2antr3 1186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ¬ 𝑤𝑅𝑤)
36		nbrne2 5079	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧 ≠ 𝑤)
37	33, 35, 36	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ≠ 𝑤)
38		eldifsn 4713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
39	32, 37, 38	sylanbrc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
40	31, 39	sylan 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
41	40	ne0d 4301	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
42		difss 4108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∖ {𝑤}) ⊆ 𝑥
43		vex 3498	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
44	43	difexi 5225	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∖ {𝑤}) ∈ V
45		fri 5512	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
46	44, 45	mpanl1 698	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
47		ssrexv 4034	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
48	42, 46, 47	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
49	26, 27, 41, 48	syl12anc 834	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
50		breq1 5062	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑢 ↔ 𝑧𝑅𝑢))
51	50	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
52	51	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
53	39, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
54	53	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55		simplr2 1212	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧𝑅𝑤)
56		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑅 Po 𝑥)
57		simplr1 1211	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧 ∈ 𝑥)
58		simplr3 1213	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑤 ∈ 𝑥)
59		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
60		potr 5481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ∧ 𝑢 ∈ 𝑥)) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
61	56, 57, 58, 59, 60	syl13anc 1368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
62	55, 61	mpand 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (𝑤𝑅𝑢 → 𝑧𝑅𝑢))
63	62	con3d 155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
64		vex 3498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
65		breq1 5062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑤𝑅𝑢))
66	65	notbid 320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
67	64, 66	ralsn 4613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
68	63, 67	syl6ibr 254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
69	54, 68	syld 47	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
70		ralun 4168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
71	70	ex 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
72	69, 71	sylcom 30	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
73		difsnid 4737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
74	73	raleqdv 3416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
75	58, 74	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
76	72, 75	sylibd 241	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
77	76	reximdva 3274	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
78	31, 77	sylan 582	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
79	49, 78	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
80	79	3exp2 1350	. . . . . . . . . . . . . 14 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑧 ∈ 𝑥 → (𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))))
81	80	rexlimdv 3283	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑧 ∈ 𝑥 𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
82	25, 81	syl5bi 244	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
83		ralnex 3236	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤)
84		breq2 5063	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝑤))
85	84	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
86	85	ralbidv 3197	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤))
87	86	rspcev 3623	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
88	87	expcom 416	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
89	83, 88	sylbir 237	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
90	82, 89	pm2.61d1 182	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
91		difsn 4725	. . . . . . . . . . . 12 ⊢ (¬ 𝑤 ∈ 𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
92	48	expr 459	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
93		neeq1 3078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
94		raleq 3406	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
95	94	rexbidv 3297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
96	93, 95	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
97	92, 96	syl5ibcom 247	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
98	97	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
99	98	adantll 712	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
100	99	impr 457	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
101	91, 100	syl5 34	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (¬ 𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
102	90, 101	pm2.61d 181	. . . . . . . . . 10 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
103	102	ex 415	. . . . . . . . 9 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
104	23, 103	syl5bi 244	. . . . . . . 8 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
105	104	alrimiv 1924	. . . . . . 7 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
106		df-fr 5509	. . . . . . 7 ⊢ (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
107	105, 106	sylibr 236	. . . . . 6 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
108	107	ex 415	. . . . 5 ⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑦 → 𝑅 Fr (𝑦 ∪ {𝑤})))
109	18, 108	sylcom 30	. . . 4 ⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤})))
110	109	a1i 11	. . 3 ⊢ (𝑦 ∈ Fin → ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
111	3, 6, 9, 12, 14, 110	findcard2 8752	. 2 ⊢ (𝐴 ∈ Fin → (𝑅 Po 𝐴 → 𝑅 Fr 𝐴))
112	111	impcom 410	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1531   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  Vcvv 3495   ∖ cdif 3933   ∪ cun 3934   ⊆ wss 3936  ∅c0 4291  {csn 4561   class class class wbr 5059   Po wpo 5467   Fr wfr 5506  Fincfn 8503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-om 7575  df-1o 8096  df-er 8283  df-en 8504  df-fin 8507

This theorem is referenced by:  fimax2g  8758  wofi  8761  fimin2g  8955  isfin1-3  9802