Theorem frfi 9288

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 5593	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Po 𝑥 ↔ 𝑅 Po ∅))
2		freq2 5648	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Fr 𝑥 ↔ 𝑅 Fr ∅))
3	1, 2	imbi12d 345	. . 3 ⊢ (𝑥 = ∅ → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4		poeq2 5593	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝑦))
5		freq2 5648	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝑦))
6	4, 5	imbi12d 345	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦 → 𝑅 Fr 𝑦)))
7		poeq2 5593	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥 ↔ 𝑅 Po (𝑦 ∪ {𝑤})))
8		freq2 5648	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥 ↔ 𝑅 Fr (𝑦 ∪ {𝑤})))
9	7, 8	imbi12d 345	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10		poeq2 5593	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝐴))
11		freq2 5648	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝐴))
12	10, 11	imbi12d 345	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴 → 𝑅 Fr 𝐴)))
13		fr0 5656	. . . 4 ⊢ 𝑅 Fr ∅
14	13	a1i 11	. . 3 ⊢ (𝑅 Po ∅ → 𝑅 Fr ∅)
15		ssun1 4173	. . . . . . 7 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑤})
16		poss 5591	. . . . . . 7 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
17	15, 16	ax-mp 5	. . . . . 6 ⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
18	17	imim1i 63	. . . . 5 ⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19		uncom 4154	. . . . . . . . . . . 12 ⊢ (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
20	19	sseq2i 4012	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21		ssundif 4488	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
22	20, 21	bitri 275	. . . . . . . . . 10 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
23	22	anbi1i 625	. . . . . . . . 9 ⊢ ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅))
24		breq1 5152	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑤 ↔ 𝑧𝑅𝑤))
25	24	cbvrexvw 3236	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 ↔ ∃𝑧 ∈ 𝑥 𝑧𝑅𝑤)
26		simpllr 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑅 Fr 𝑦)
27		simplrl 776	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28		poss 5591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
29	28	impcom 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
30	22, 29	sylan2br 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
31	30	ad2ant2r 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32		simpr1 1195	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
33		simpr2 1196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧𝑅𝑤)
34		poirr 5601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ 𝑤 ∈ 𝑥) → ¬ 𝑤𝑅𝑤)
35	34	3ad2antr3 1191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ¬ 𝑤𝑅𝑤)
36		nbrne2 5169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧 ≠ 𝑤)
37	33, 35, 36	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ≠ 𝑤)
38		eldifsn 4791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
39	32, 37, 38	sylanbrc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
40	31, 39	sylan 581	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
41	40	ne0d 4336	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
42		difss 4132	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∖ {𝑤}) ⊆ 𝑥
43		vex 3479	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
44	43	difexi 5329	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∖ {𝑤}) ∈ V
45		fri 5637	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
46	44, 45	mpanl1 699	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
47		ssrexv 4052	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
48	42, 46, 47	mpsyl 68	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
49	26, 27, 41, 48	syl12anc 836	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
50		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑢 ↔ 𝑧𝑅𝑢))
51	50	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
52	51	rspcv 3609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
53	39, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
54	53	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55		simplr2 1217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧𝑅𝑤)
56		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑅 Po 𝑥)
57		simplr1 1216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧 ∈ 𝑥)
58		simplr3 1218	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑤 ∈ 𝑥)
59		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
60		potr 5602	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ∧ 𝑢 ∈ 𝑥)) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
61	56, 57, 58, 59, 60	syl13anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
62	55, 61	mpand 694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (𝑤𝑅𝑢 → 𝑧𝑅𝑢))
63	62	con3d 152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
64		vex 3479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
65		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑤𝑅𝑢))
66	65	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
67	64, 66	ralsn 4686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
68	63, 67	imbitrrdi 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
69	54, 68	syld 47	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
70		ralun 4193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
71	70	ex 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
72	69, 71	sylcom 30	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
73		difsnid 4814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
74	73	raleqdv 3326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
75	58, 74	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
76	72, 75	sylibd 238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
77	76	reximdva 3169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
78	31, 77	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
79	49, 78	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
80	79	3exp2 1355	. . . . . . . . . . . . . 14 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑧 ∈ 𝑥 → (𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))))
81	80	rexlimdv 3154	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑧 ∈ 𝑥 𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
82	25, 81	biimtrid 241	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
83		ralnex 3073	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤)
84		breq2 5153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝑤))
85	84	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
86	85	ralbidv 3178	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤))
87	86	rspcev 3613	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
88	87	expcom 415	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
89	83, 88	sylbir 234	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
90	82, 89	pm2.61d1 180	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
91		difsn 4802	. . . . . . . . . . . 12 ⊢ (¬ 𝑤 ∈ 𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
92	48	expr 458	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
93		neeq1 3004	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
94		raleq 3323	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
95	94	rexbidv 3179	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
96	93, 95	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
97	92, 96	syl5ibcom 244	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
98	97	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
99	98	adantll 713	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
100	99	impr 456	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
101	91, 100	syl5 34	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (¬ 𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
102	90, 101	pm2.61d 179	. . . . . . . . . 10 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
103	102	ex 414	. . . . . . . . 9 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
104	23, 103	biimtrid 241	. . . . . . . 8 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
105	104	alrimiv 1931	. . . . . . 7 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
106		df-fr 5632	. . . . . . 7 ⊢ (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
107	105, 106	sylibr 233	. . . . . 6 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
108	107	ex 414	. . . . 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 9164	. 2 ⊢ (𝐴 ∈ Fin → (𝑅 Po 𝐴 → 𝑅 Fr 𝐴))
112	111	impcom 409	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  ∀wal 1540   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∖ cdif 3946   ∪ cun 3947   ⊆ wss 3949  ∅c0 4323  {csn 4629   class class class wbr 5149   Po wpo 5587   Fr wfr 5629  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7856  df-en 8940  df-fin 8943

This theorem is referenced by:  fimax2g  9289  wofi  9292  fimin2g  9492  isfin1-3  10381