wofib

Description: The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014) (Revised by Mario Carneiro, 23-May-2015)

		Ref	Expression
	Hypothesis	wofib.1	$⊢ A \in V$
	Assertion	wofib	$⊢ (R Or A \land A \in Fin) \leftrightarrow (R We A \land R^{-1} We A)$

Proof

Step	Hyp	Ref	Expression
1		wofib.1	$⊢ A \in V$
2		wofi	$⊢ (R Or A \land A \in Fin) \to R We A$
3		cnvso	$⊢ R Or A \leftrightarrow R^{-1} Or A$
4		wofi	$⊢ (R^{-1} Or A \land A \in Fin) \to R^{-1} We A$
5	3 4	sylanb	$⊢ (R Or A \land A \in Fin) \to R^{-1} We A$
6	2 5	jca	$⊢ (R Or A \land A \in Fin) \to (R We A \land R^{-1} We A)$
7		weso	$⊢ R We A \to R Or A$
8	7	adantr	$⊢ (R We A \land R^{-1} We A) \to R Or A$
9		peano2	$⊢ y \in ω \to suc y \in ω$
10		sucidg	$⊢ y \in ω \to y \in suc y$
11		vex	$⊢ z \in V$
12		vex	$⊢ y \in V$
13	11 12	brcnv	$⊢ z E^{-1} y \leftrightarrow y E z$
14		epel	$⊢ y E z \leftrightarrow y \in z$
15	13 14	bitri	$⊢ z E^{-1} y \leftrightarrow y \in z$
16		eleq2	$⊢ z = suc y \to (y \in z \leftrightarrow y \in suc y)$
17	15 16	bitrid	$⊢ z = suc y \to (z E^{-1} y \leftrightarrow y \in suc y)$
18	17	rspcev	$⊢ (suc y \in ω \land y \in suc y) \to \exists z \in ω z E^{-1} y$
19	9 10 18	syl2anc	$⊢ y \in ω \to \exists z \in ω z E^{-1} y$
20		dfrex2	$⊢ \exists z \in ω z E^{-1} y \leftrightarrow \neg \forall z \in ω \neg z E^{-1} y$
21	19 20	sylib	$⊢ y \in ω \to \neg \forall z \in ω \neg z E^{-1} y$
22	21	nrex	$⊢ \neg \exists y \in ω \forall z \in ω \neg z E^{-1} y$
23		ordom	$⊢ Ord ω$
24		eqid	$⊢ OrdIso (R, A) = OrdIso (R, A)$
25	24	oicl	$⊢ Ord dom OrdIso (R, A)$
26		ordtri1	$⊢ (Ord ω \land Ord dom OrdIso (R, A)) \to (ω \subseteq dom OrdIso (R, A) \leftrightarrow \neg dom OrdIso (R, A) \in ω)$
27	23 25 26	mp2an	$⊢ ω \subseteq dom OrdIso (R, A) \leftrightarrow \neg dom OrdIso (R, A) \in ω$
28	24	oion	$⊢ A \in V \to dom OrdIso (R, A) \in On$
29	1 28	mp1i	$⊢ ((R We A \land R^{-1} We A) \land ω \subseteq dom OrdIso (R, A)) \to dom OrdIso (R, A) \in On$
30		simpr	$⊢ ((R We A \land R^{-1} We A) \land ω \subseteq dom OrdIso (R, A)) \to ω \subseteq dom OrdIso (R, A)$
31	29 30	ssexd	$⊢ ((R We A \land R^{-1} We A) \land ω \subseteq dom OrdIso (R, A)) \to ω \in V$
32	24	oiiso	$⊢ (A \in V \land R We A) \to OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A)$
33	1 32	mpan	$⊢ R We A \to OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A)$
34		isocnv2	$⊢ OrdIso (R, A) {Isom}_{E, R} (dom OrdIso (R, A), A) \leftrightarrow OrdIso (R, A) {Isom}_{E^{-1}, R^{-1}} (dom OrdIso (R, A), A)$
35	33 34	sylib	$⊢ R We A \to OrdIso (R, A) {Isom}_{E^{-1}, R^{-1}} (dom OrdIso (R, A), A)$
36		wefr	$⊢ R^{-1} We A \to R^{-1} Fr A$
37		isofr	$⊢ OrdIso (R, A) {Isom}_{E^{-1}, R^{-1}} (dom OrdIso (R, A), A) \to (E^{-1} Fr dom OrdIso (R, A) \leftrightarrow R^{-1} Fr A)$
38	37	biimpar	$⊢ (OrdIso (R, A) {Isom}_{E^{-1}, R^{-1}} (dom OrdIso (R, A), A) \land R^{-1} Fr A) \to E^{-1} Fr dom OrdIso (R, A)$
39	35 36 38	syl2an	$⊢ (R We A \land R^{-1} We A) \to E^{-1} Fr dom OrdIso (R, A)$
40	39	adantr	$⊢ ((R We A \land R^{-1} We A) \land ω \subseteq dom OrdIso (R, A)) \to E^{-1} Fr dom OrdIso (R, A)$
41		1onn	$⊢ 1_{𝑜} \in ω$
42		ne0i	$⊢ 1_{𝑜} \in ω \to ω \neq \emptyset$
43	41 42	mp1i	$⊢ ((R We A \land R^{-1} We A) \land ω \subseteq dom OrdIso (R, A)) \to ω \neq \emptyset$
44		fri	$⊢ ((ω \in V \land E^{-1} Fr dom OrdIso (R, A)) \land (ω \subseteq dom OrdIso (R, A) \land ω \neq \emptyset)) \to \exists y \in ω \forall z \in ω \neg z E^{-1} y$
45	31 40 30 43 44	syl22anc	$⊢ ((R We A \land R^{-1} We A) \land ω \subseteq dom OrdIso (R, A)) \to \exists y \in ω \forall z \in ω \neg z E^{-1} y$
46	45	ex	$⊢ (R We A \land R^{-1} We A) \to (ω \subseteq dom OrdIso (R, A) \to \exists y \in ω \forall z \in ω \neg z E^{-1} y)$
47	27 46	biimtrrid	$⊢ (R We A \land R^{-1} We A) \to (\neg dom OrdIso (R, A) \in ω \to \exists y \in ω \forall z \in ω \neg z E^{-1} y)$
48	22 47	mt3i	$⊢ (R We A \land R^{-1} We A) \to dom OrdIso (R, A) \in ω$
49		ssid	$⊢ dom OrdIso (R, A) \subseteq dom OrdIso (R, A)$
50		ssnnfi	$⊢ (dom OrdIso (R, A) \in ω \land dom OrdIso (R, A) \subseteq dom OrdIso (R, A)) \to dom OrdIso (R, A) \in Fin$
51	48 49 50	sylancl	$⊢ (R We A \land R^{-1} We A) \to dom OrdIso (R, A) \in Fin$
52		simpl	$⊢ (R We A \land R^{-1} We A) \to R We A$
53	24	oien	$⊢ (A \in V \land R We A) \to dom OrdIso (R, A) \approx A$
54	1 52 53	sylancr	$⊢ (R We A \land R^{-1} We A) \to dom OrdIso (R, A) \approx A$
55		enfi	$⊢ dom OrdIso (R, A) \approx A \to (dom OrdIso (R, A) \in Fin \leftrightarrow A \in Fin)$
56	54 55	syl	$⊢ (R We A \land R^{-1} We A) \to (dom OrdIso (R, A) \in Fin \leftrightarrow A \in Fin)$
57	51 56	mpbid	$⊢ (R We A \land R^{-1} We A) \to A \in Fin$
58	8 57	jca	$⊢ (R We A \land R^{-1} We A) \to (R Or A \land A \in Fin)$
59	6 58	impbii	$⊢ (R Or A \land A \in Fin) \leftrightarrow (R We A \land R^{-1} We A)$

Metamath Proof Explorer

Theorem wofib

Proof