isfin4p1

Description: Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 can be assumed to be only a singleton smaller than the original.) (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	isfin4p1	$⊢ A \in {Fin}^{IV} \leftrightarrow A ≺ (A ⊔︀ 1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		1on	$⊢ 1_{𝑜} \in On$
2		djudoml	$⊢ (A \in {Fin}^{IV} \land 1_{𝑜} \in On) \to A ≼ (A ⊔︀ 1_{𝑜})$
3	1 2	mpan2	$⊢ A \in {Fin}^{IV} \to A ≼ (A ⊔︀ 1_{𝑜})$
4		1oex	$⊢ 1_{𝑜} \in V$
5	4	snid	$⊢ 1_{𝑜} \in \{1_{𝑜}\}$
6		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
7		opelxpi	$⊢ (1_{𝑜} \in \{1_{𝑜}\} \land \emptyset \in 1_{𝑜}) \to ⟨1_{𝑜}, \emptyset⟩ \in (\{1_{𝑜}\} \times 1_{𝑜})$
8	5 6 7	mp2an	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in (\{1_{𝑜}\} \times 1_{𝑜})$
9		elun2	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in (\{1_{𝑜}\} \times 1_{𝑜}) \to ⟨1_{𝑜}, \emptyset⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}))$
10	8 9	ax-mp	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}))$
11		df-dju	$⊢ (A ⊔︀ 1_{𝑜}) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
12	10 11	eleqtrri	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in (A ⊔︀ 1_{𝑜})$
13		1n0	$⊢ 1_{𝑜} \neq \emptyset$
14		opelxp1	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in (\{\emptyset\} \times A) \to 1_{𝑜} \in \{\emptyset\}$
15		elsni	$⊢ 1_{𝑜} \in \{\emptyset\} \to 1_{𝑜} = \emptyset$
16	14 15	syl	$⊢ ⟨1_{𝑜}, \emptyset⟩ \in (\{\emptyset\} \times A) \to 1_{𝑜} = \emptyset$
17	16	necon3ai	$⊢ 1_{𝑜} \neq \emptyset \to \neg ⟨1_{𝑜}, \emptyset⟩ \in (\{\emptyset\} \times A)$
18	13 17	ax-mp	$⊢ \neg ⟨1_{𝑜}, \emptyset⟩ \in (\{\emptyset\} \times A)$
19		ssun1	$⊢ \{\emptyset\} \times A \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
20	19 11	sseqtrri	$⊢ \{\emptyset\} \times A \subseteq (A ⊔︀ 1_{𝑜})$
21		ssnelpss	$⊢ \{\emptyset\} \times A \subseteq (A ⊔︀ 1_{𝑜}) \to ((⟨1_{𝑜}, \emptyset⟩ \in (A ⊔︀ 1_{𝑜}) \land \neg ⟨1_{𝑜}, \emptyset⟩ \in (\{\emptyset\} \times A)) \to \{\emptyset\} \times A \subset (A ⊔︀ 1_{𝑜}))$
22	20 21	ax-mp	$⊢ (⟨1_{𝑜}, \emptyset⟩ \in (A ⊔︀ 1_{𝑜}) \land \neg ⟨1_{𝑜}, \emptyset⟩ \in (\{\emptyset\} \times A)) \to \{\emptyset\} \times A \subset (A ⊔︀ 1_{𝑜})$
23	12 18 22	mp2an	$⊢ \{\emptyset\} \times A \subset (A ⊔︀ 1_{𝑜})$
24		0ex	$⊢ \emptyset \in V$
25		relen	$⊢ Rel \approx$
26	25	brrelex1i	$⊢ A \approx (A ⊔︀ 1_{𝑜}) \to A \in V$
27		xpsnen2g	$⊢ (\emptyset \in V \land A \in V) \to (\{\emptyset\} \times A) \approx A$
28	24 26 27	sylancr	$⊢ A \approx (A ⊔︀ 1_{𝑜}) \to (\{\emptyset\} \times A) \approx A$
29		entr	$⊢ ((\{\emptyset\} \times A) \approx A \land A \approx (A ⊔︀ 1_{𝑜})) \to (\{\emptyset\} \times A) \approx (A ⊔︀ 1_{𝑜})$
30	28 29	mpancom	$⊢ A \approx (A ⊔︀ 1_{𝑜}) \to (\{\emptyset\} \times A) \approx (A ⊔︀ 1_{𝑜})$
31		fin4i	$⊢ (\{\emptyset\} \times A \subset (A ⊔︀ 1_{𝑜}) \land (\{\emptyset\} \times A) \approx (A ⊔︀ 1_{𝑜})) \to \neg (A ⊔︀ 1_{𝑜}) \in {Fin}^{IV}$
32	23 30 31	sylancr	$⊢ A \approx (A ⊔︀ 1_{𝑜}) \to \neg (A ⊔︀ 1_{𝑜}) \in {Fin}^{IV}$
33		fin4en1	$⊢ A \approx (A ⊔︀ 1_{𝑜}) \to (A \in {Fin}^{IV} \to (A ⊔︀ 1_{𝑜}) \in {Fin}^{IV})$
34	32 33	mtod	$⊢ A \approx (A ⊔︀ 1_{𝑜}) \to \neg A \in {Fin}^{IV}$
35	34	con2i	$⊢ A \in {Fin}^{IV} \to \neg A \approx (A ⊔︀ 1_{𝑜})$
36		brsdom	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \leftrightarrow (A ≼ (A ⊔︀ 1_{𝑜}) \land \neg A \approx (A ⊔︀ 1_{𝑜}))$
37	3 35 36	sylanbrc	$⊢ A \in {Fin}^{IV} \to A ≺ (A ⊔︀ 1_{𝑜})$
38		sdomnen	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to \neg A \approx (A ⊔︀ 1_{𝑜})$
39		infdju1	$⊢ ω ≼ A \to (A ⊔︀ 1_{𝑜}) \approx A$
40	39	ensymd	$⊢ ω ≼ A \to A \approx (A ⊔︀ 1_{𝑜})$
41	38 40	nsyl	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to \neg ω ≼ A$
42		relsdom	$⊢ Rel ≺$
43	42	brrelex1i	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to A \in V$
44		isfin4-2	$⊢ A \in V \to (A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ A)$
45	43 44	syl	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to (A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ A)$
46	41 45	mpbird	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to A \in {Fin}^{IV}$
47	37 46	impbii	$⊢ A \in {Fin}^{IV} \leftrightarrow A ≺ (A ⊔︀ 1_{𝑜})$

Metamath Proof Explorer

Theorem isfin4p1

Proof