Theorem frfi 8090

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 4963	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Po 𝑥 ↔ 𝑅 Po ∅))
2		freq2 5009	. . . 4 ⊢ (𝑥 = ∅ → (𝑅 Fr 𝑥 ↔ 𝑅 Fr ∅))
3	1, 2	imbi12d 333	. . 3 ⊢ (𝑥 = ∅ → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4		poeq2 4963	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝑦))
5		freq2 5009	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝑦))
6	4, 5	imbi12d 333	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦 → 𝑅 Fr 𝑦)))
7		poeq2 4963	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥 ↔ 𝑅 Po (𝑦 ∪ {𝑤})))
8		freq2 5009	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥 ↔ 𝑅 Fr (𝑦 ∪ {𝑤})))
9	7, 8	imbi12d 333	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10		poeq2 4963	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝐴))
11		freq2 5009	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝐴))
12	10, 11	imbi12d 333	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴 → 𝑅 Fr 𝐴)))
13		fr0 5017	. . . 4 ⊢ 𝑅 Fr ∅
14	13	a1i 11	. . 3 ⊢ (𝑅 Po ∅ → 𝑅 Fr ∅)
15		ssun1 3738	. . . . . . 7 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑤})
16		poss 4961	. . . . . . 7 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
17	15, 16	ax-mp 5	. . . . . 6 ⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
18	17	imim1i 61	. . . . 5 ⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19		uncom 3719	. . . . . . . . . . . 12 ⊢ (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
20	19	sseq2i 3593	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21		ssundif 4004	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
22	20, 21	bitri 263	. . . . . . . . . 10 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
23	22	anbi1i 727	. . . . . . . . 9 ⊢ ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅))
24		breq1 4586	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑤 ↔ 𝑧𝑅𝑤))
25	24	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 ↔ ∃𝑧 ∈ 𝑥 𝑧𝑅𝑤)
26		simpllr 795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑅 Fr 𝑦)
27		simplrl 796	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28		poss 4961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
29	28	impcom 445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
30	22, 29	sylan2br 492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
31	30	ad2ant2r 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32		simpr1 1060	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ 𝑥)
33		simpr2 1061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧𝑅𝑤)
34		poirr 4970	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ 𝑤 ∈ 𝑥) → ¬ 𝑤𝑅𝑤)
35	34	3ad2antr3 1221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ¬ 𝑤𝑅𝑤)
36		nbrne2 4603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧 ≠ 𝑤)
37	33, 35, 36	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ≠ 𝑤)
38		eldifsn 4260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
39	32, 37, 38	sylanbrc 695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
40	31, 39	sylan 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
41		ne0i 3880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) → (𝑥 ∖ {𝑤}) ≠ ∅)
42	40, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
43		difss 3699	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∖ {𝑤}) ⊆ 𝑥
44		vex 3176	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
45		difexg 4735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ V → (𝑥 ∖ {𝑤}) ∈ V)
46	44, 45	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∖ {𝑤}) ∈ V
47		fri 5000	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
48	46, 47	mpanl1 712	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
49		ssrexv 3630	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
50	43, 48, 49	mpsyl 66	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
51	26, 27, 42, 50	syl12anc 1316	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
52		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑢 ↔ 𝑧𝑅𝑢))
53	52	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
54	53	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55	39, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
56	55	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
57		simplr2 1097	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧𝑅𝑤)
58		simpll 786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑅 Po 𝑥)
59		simplr1 1096	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧 ∈ 𝑥)
60		simplr3 1098	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑤 ∈ 𝑥)
61		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥)
62		potr 4971	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ∧ 𝑢 ∈ 𝑥)) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
63	58, 59, 60, 61, 62	syl13anc 1320	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢))
64	57, 63	mpand 707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (𝑤𝑅𝑢 → 𝑧𝑅𝑢))
65	64	con3d 147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
66		vex 3176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
67		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑤𝑅𝑢))
68	67	notbid 307	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
69	66, 68	ralsn 4169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
70	65, 69	syl6ibr 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
71	56, 70	syld 46	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
72		ralun 3757	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
73	72	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
74	71, 73	sylcom 30	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
75		difsnid 4282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
76	75	raleqdv 3121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
77	60, 76	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
78	74, 77	sylibd 228	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
79	78	reximdva 3000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
80	31, 79	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
81	51, 80	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
82	81	3exp2 1277	. . . . . . . . . . . . . 14 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑧 ∈ 𝑥 → (𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))))
83	82	rexlimdv 3012	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑧 ∈ 𝑥 𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
84	25, 83	syl5bi 231	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
85		ralnex 2975	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤)
86		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝑤))
87	86	notbid 307	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
88	87	ralbidv 2969	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑤 → (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤))
89	88	rspcev 3282	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
90	89	expcom 450	. . . . . . . . . . . . 13 ⊢ (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
91	85, 90	sylbir 224	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
92	84, 91	pm2.61d1 170	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
93		difsn 4269	. . . . . . . . . . . 12 ⊢ (¬ 𝑤 ∈ 𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
94	50	expr 641	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
95		neeq1 2844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
96		raleq 3115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
97	96	rexbidv 3034	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
98	95, 97	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
99	94, 98	syl5ibcom 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
100	99	com23 84	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
101	100	adantll 746	. . . . . . . . . . . . 13 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))
102	101	impr 647	. . . . . . . . . . . 12 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
103	93, 102	syl5 33	. . . . . . . . . . 11 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (¬ 𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
104	92, 103	pm2.61d 169	. . . . . . . . . 10 ⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)
105	104	ex 449	. . . . . . . . 9 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
106	23, 105	syl5bi 231	. . . . . . . 8 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
107	106	alrimiv 1842	. . . . . . 7 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
108		df-fr 4997	. . . . . . 7 ⊢ (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))
109	107, 108	sylibr 223	. . . . . 6 ⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
110	109	ex 449	. . . . 5 ⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑦 → 𝑅 Fr (𝑦 ∪ {𝑤})))
111	18, 110	sylcom 30	. . . 4 ⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤})))
112	111	a1i 11	. . 3 ⊢ (𝑦 ∈ Fin → ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
113	3, 6, 9, 12, 14, 112	findcard2 8085	. 2 ⊢ (𝐴 ∈ Fin → (𝑅 Po 𝐴 → 𝑅 Fr 𝐴))
114	113	impcom 445	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583   Po wpo 4957   Fr wfr 4994  Fincfn 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-1o 7447  df-er 7629  df-en 7842  df-fin 7845

This theorem is referenced by:  fimax2g  8091  wofi  8094  fimin2g  8286  isfin1-3  9091