Theorem frfi 9284

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 5591	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Po 𝑥 ↔ 𝑅 Po ∅))
2		freq2 5646	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Fr 𝑥 ↔ 𝑅 Fr ∅))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = ∅ → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4		poeq2 5591	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝑦))
5		freq2 5646	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝑦))
6	4, 5	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦 → 𝑅 Fr 𝑦)))
7		poeq2 5591	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥 ↔ 𝑅 Po (𝑦 ∪ {𝑤})))
8		freq2 5646	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥 ↔ 𝑅 Fr (𝑦 ∪ {𝑤})))
9	7, 8	imbi12d 344	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10		poeq2 5591	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝐴))
11		freq2 5646	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝐴))
12	10, 11	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴 → 𝑅 Fr 𝐴)))
13		fr0 5654	. . . 4 ⊢ 𝑅 Fr ∅
14	13	a1i 11	. . 3 ⊢ (𝑅 Po ∅ → 𝑅 Fr ∅)
15		ssun1 4171	. . . . . . 7 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑤})
16		poss 5589	. . . . . . 7 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
17	15, 16	ax-mp 5	. . . . . 6 ⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
18	17	imim1i 63	. . . . 5 ⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19		uncom 4152	. . . . . . . . . . . 12 ⊢ (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
20	19	sseq2i 4010	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21		ssundif 4486	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
22	20, 21	bitri 274	. . . . . . . . . 10 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
23	22	anbi1i 624	. . . . . . . . 9 ⊢ ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅))
24		breq1 5150	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑤 ↔ 𝑧𝑅𝑤))
25	24	cbvrexvw 3235	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 ↔ ∃𝑧 ∈ 𝑥 𝑧𝑅𝑤)
26		simpllr 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑅 Fr 𝑦)
27		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28		poss 5589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
29	28	impcom 408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
30	22, 29	sylan2br 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
31	30	ad2ant2r 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32		simpr1 1194	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
33		simpr2 1195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧𝑅𝑤)
34		poirr 5599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ 𝑤 ∈ 𝑥) → ¬ 𝑤𝑅𝑤)
35	34	3ad2antr3 1190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ¬ 𝑤𝑅𝑤)
36		nbrne2 5167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧 ≠ 𝑤)
37	33, 35, 36	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ≠ 𝑤)
38		eldifsn 4789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
39	32, 37, 38	sylanbrc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
40	31, 39	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
41	40	ne0d 4334	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
42		difss 4130	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∖ {𝑤}) ⊆ 𝑥
43		vex 3478	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
44	43	difexi 5327	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∖ {𝑤}) ∈ V
45		fri 5635	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
46	44, 45	mpanl1 698	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
47		ssrexv 4050	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
48	42, 46, 47	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
49	26, 27, 41, 48	syl12anc 835	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
50		breq1 5150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑢 ↔ 𝑧𝑅𝑢))
51	50	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
52	51	rspcv 3608	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
53	39, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
54	53	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55		simplr2 1216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧𝑅𝑤)
56		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑅 Po 𝑥)
57		simplr1 1215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧 ∈ 𝑥)
58		simplr3 1217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑤 ∈ 𝑥)
59		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
60		potr 5600	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ∧ 𝑢 ∈ 𝑥)) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
61	56, 57, 58, 59, 60	syl13anc 1372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
62	55, 61	mpand 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (𝑤𝑅𝑢 → 𝑧𝑅𝑢))
63	62	con3d 152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
64		vex 3478	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
65		breq1 5150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑤𝑅𝑢))
66	65	notbid 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
67	64, 66	ralsn 4684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
68	63, 67	syl6ibr 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
69	54, 68	syld 47	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
70		ralun 4191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
71	70	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
72	69, 71	sylcom 30	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
73		difsnid 4812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
74	73	raleqdv 3325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
75	58, 74	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
76	72, 75	sylibd 238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
77	76	reximdva 3168	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
78	31, 77	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
79	49, 78	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
80	79	3exp2 1354	. . . . . . . . . . . . . 14 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑧 ∈ 𝑥 → (𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))))
81	80	rexlimdv 3153	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑧 ∈ 𝑥 𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
82	25, 81	biimtrid 241	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
83		ralnex 3072	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤)
84		breq2 5151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝑤))
85	84	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
86	85	ralbidv 3177	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤))
87	86	rspcev 3612	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
88	87	expcom 414	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
89	83, 88	sylbir 234	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
90	82, 89	pm2.61d1 180	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
91		difsn 4800	. . . . . . . . . . . 12 ⊢ (¬ 𝑤 ∈ 𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
92	48	expr 457	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
93		neeq1 3003	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
94		raleq 3322	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
95	94	rexbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
96	93, 95	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
97	92, 96	syl5ibcom 244	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
98	97	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
99	98	adantll 712	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
100	99	impr 455	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
101	91, 100	syl5 34	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (¬ 𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
102	90, 101	pm2.61d 179	. . . . . . . . . 10 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
103	102	ex 413	. . . . . . . . 9 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
104	23, 103	biimtrid 241	. . . . . . . 8 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
105	104	alrimiv 1930	. . . . . . 7 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
106		df-fr 5630	. . . . . . 7 ⊢ (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
107	105, 106	sylibr 233	. . . . . 6 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
108	107	ex 413	. . . . 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 9160	. 2 ⊢ (𝐴 ∈ Fin → (𝑅 Po 𝐴 → 𝑅 Fr 𝐴))
112	111	impcom 408	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  Vcvv 3474   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947  ∅c0 4321  {csn 4627   class class class wbr 5147   Po wpo 5585   Fr wfr 5627  Fincfn 8935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7852  df-en 8936  df-fin 8939

This theorem is referenced by:  fimax2g  9285  wofi  9288  fimin2g  9488  isfin1-3  10377