isfin7-2

Description: A set is VII-finite iff it is non-well-orderable or finite. (Contributed by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	isfin7-2	$⊢ A \in V \to (A \in {Fin}^{VII} \leftrightarrow (A \in dom card \to A \in Fin))$

Proof

Step	Hyp	Ref	Expression
1		isfin7	$⊢ A \in {Fin}^{VII} \to (A \in {Fin}^{VII} \leftrightarrow \neg \exists x \in (On ∖ ω) A \approx x)$
2	1	ibi	$⊢ A \in {Fin}^{VII} \to \neg \exists x \in (On ∖ ω) A \approx x$
3		isnum2	$⊢ A \in dom card \leftrightarrow \exists x \in On x \approx A$
4		ensym	$⊢ x \approx A \to A \approx x$
5		simprl	$⊢ (\neg A \in Fin \land (x \in On \land A \approx x)) \to x \in On$
6		enfi	$⊢ A \approx x \to (A \in Fin \leftrightarrow x \in Fin)$
7		onfin	$⊢ x \in On \to (x \in Fin \leftrightarrow x \in ω)$
8	6 7	sylan9bbr	$⊢ (x \in On \land A \approx x) \to (A \in Fin \leftrightarrow x \in ω)$
9	8	biimprd	$⊢ (x \in On \land A \approx x) \to (x \in ω \to A \in Fin)$
10	9	con3d	$⊢ (x \in On \land A \approx x) \to (\neg A \in Fin \to \neg x \in ω)$
11	10	impcom	$⊢ (\neg A \in Fin \land (x \in On \land A \approx x)) \to \neg x \in ω$
12	5 11	eldifd	$⊢ (\neg A \in Fin \land (x \in On \land A \approx x)) \to x \in (On ∖ ω)$
13		simprr	$⊢ (\neg A \in Fin \land (x \in On \land A \approx x)) \to A \approx x$
14	12 13	jca	$⊢ (\neg A \in Fin \land (x \in On \land A \approx x)) \to (x \in (On ∖ ω) \land A \approx x)$
15	4 14	sylanr2	$⊢ (\neg A \in Fin \land (x \in On \land x \approx A)) \to (x \in (On ∖ ω) \land A \approx x)$
16	15	ex	$⊢ \neg A \in Fin \to ((x \in On \land x \approx A) \to (x \in (On ∖ ω) \land A \approx x))$
17	16	reximdv2	$⊢ \neg A \in Fin \to (\exists x \in On x \approx A \to \exists x \in (On ∖ ω) A \approx x)$
18	17	com12	$⊢ \exists x \in On x \approx A \to (\neg A \in Fin \to \exists x \in (On ∖ ω) A \approx x)$
19	3 18	sylbi	$⊢ A \in dom card \to (\neg A \in Fin \to \exists x \in (On ∖ ω) A \approx x)$
20	19	con1d	$⊢ A \in dom card \to (\neg \exists x \in (On ∖ ω) A \approx x \to A \in Fin)$
21	2 20	syl5com	$⊢ A \in {Fin}^{VII} \to (A \in dom card \to A \in Fin)$
22		eldifi	$⊢ x \in (On ∖ ω) \to x \in On$
23		ensym	$⊢ A \approx x \to x \approx A$
24		isnumi	$⊢ (x \in On \land x \approx A) \to A \in dom card$
25	22 23 24	syl2an	$⊢ (x \in (On ∖ ω) \land A \approx x) \to A \in dom card$
26	25	rexlimiva	$⊢ \exists x \in (On ∖ ω) A \approx x \to A \in dom card$
27	26	con3i	$⊢ \neg A \in dom card \to \neg \exists x \in (On ∖ ω) A \approx x$
28		isfin7	$⊢ A \in V \to (A \in {Fin}^{VII} \leftrightarrow \neg \exists x \in (On ∖ ω) A \approx x)$
29	27 28	imbitrrid	$⊢ A \in V \to (\neg A \in dom card \to A \in {Fin}^{VII})$
30		fin17	$⊢ A \in Fin \to A \in {Fin}^{VII}$
31	30	a1i	$⊢ A \in V \to (A \in Fin \to A \in {Fin}^{VII})$
32	29 31	jad	$⊢ A \in V \to ((A \in dom card \to A \in Fin) \to A \in {Fin}^{VII})$
33	21 32	impbid2	$⊢ A \in V \to (A \in {Fin}^{VII} \leftrightarrow (A \in dom card \to A \in Fin))$

Metamath Proof Explorer

Theorem isfin7-2

Proof