fin2so

Description: Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019)

		Ref	Expression
	Assertion	fin2so	$⊢ (A \in {Fin}^{II} \land R Or A) \to A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to A \in {Fin}^{II}$
2		ssrab2	$⊢ \{w \in x \| w R v\} \subseteq x$
3		sstr	$⊢ (\{w \in x \| w R v\} \subseteq x \land x \subseteq A) \to \{w \in x \| w R v\} \subseteq A$
4	2 3	mpan	$⊢ x \subseteq A \to \{w \in x \| w R v\} \subseteq A$
5		elpw2g	$⊢ A \in {Fin}^{II} \to (\{w \in x \| w R v\} \in 𝒫 A \leftrightarrow \{w \in x \| w R v\} \subseteq A)$
6	5	biimpar	$⊢ (A \in {Fin}^{II} \land \{w \in x \| w R v\} \subseteq A) \to \{w \in x \| w R v\} \in 𝒫 A$
7	4 6	sylan2	$⊢ (A \in {Fin}^{II} \land x \subseteq A) \to \{w \in x \| w R v\} \in 𝒫 A$
8	7	ralrimivw	$⊢ (A \in {Fin}^{II} \land x \subseteq A) \to \forall v \in x \{w \in x \| w R v\} \in 𝒫 A$
9		vex	$⊢ x \in V$
10	9	rabex	$⊢ \{w \in x \| w R v\} \in V$
11	10	rgenw	$⊢ \forall v \in x \{w \in x \| w R v\} \in V$
12		eqid	$⊢ (v \in x ⟼ \{w \in x \| w R v\}) = (v \in x ⟼ \{w \in x \| w R v\})$
13		eleq1	$⊢ y = \{w \in x \| w R v\} \to (y \in 𝒫 A \leftrightarrow \{w \in x \| w R v\} \in 𝒫 A)$
14	12 13	ralrnmptw	$⊢ \forall v \in x \{w \in x \| w R v\} \in V \to (\forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) y \in 𝒫 A \leftrightarrow \forall v \in x \{w \in x \| w R v\} \in 𝒫 A)$
15	11 14	ax-mp	$⊢ \forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) y \in 𝒫 A \leftrightarrow \forall v \in x \{w \in x \| w R v\} \in 𝒫 A$
16	8 15	sylibr	$⊢ (A \in {Fin}^{II} \land x \subseteq A) \to \forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) y \in 𝒫 A$
17		dfss3	$⊢ ran (v \in x ⟼ \{w \in x \| w R v\}) \subseteq 𝒫 A \leftrightarrow \forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) y \in 𝒫 A$
18	16 17	sylibr	$⊢ (A \in {Fin}^{II} \land x \subseteq A) \to ran (v \in x ⟼ \{w \in x \| w R v\}) \subseteq 𝒫 A$
19	18	adantlr	$⊢ ((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \to ran (v \in x ⟼ \{w \in x \| w R v\}) \subseteq 𝒫 A$
20	19	adantr	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to ran (v \in x ⟼ \{w \in x \| w R v\}) \subseteq 𝒫 A$
21	10 12	dmmpti	$⊢ dom (v \in x ⟼ \{w \in x \| w R v\}) = x$
22	21	neeq1i	$⊢ dom (v \in x ⟼ \{w \in x \| w R v\}) \neq \emptyset \leftrightarrow x \neq \emptyset$
23		dm0rn0	$⊢ dom (v \in x ⟼ \{w \in x \| w R v\}) = \emptyset \leftrightarrow ran (v \in x ⟼ \{w \in x \| w R v\}) = \emptyset$
24	23	necon3bii	$⊢ dom (v \in x ⟼ \{w \in x \| w R v\}) \neq \emptyset \leftrightarrow ran (v \in x ⟼ \{w \in x \| w R v\}) \neq \emptyset$
25	22 24	sylbb1	$⊢ x \neq \emptyset \to ran (v \in x ⟼ \{w \in x \| w R v\}) \neq \emptyset$
26	25	adantl	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to ran (v \in x ⟼ \{w \in x \| w R v\}) \neq \emptyset$
27		soss	$⊢ x \subseteq A \to (R Or A \to R Or x)$
28	27	impcom	$⊢ (R Or A \land x \subseteq A) \to R Or x$
29		porpss	$⊢ [\subset] Po ran (v \in x ⟼ \{w \in x \| w R v\})$
30	29	a1i	$⊢ R Or x \to [\subset] Po ran (v \in x ⟼ \{w \in x \| w R v\})$
31		solin	$⊢ (R Or x \land (v \in x \land y \in x)) \to (v R y \lor v = y \lor y R v)$
32		fin2solem	$⊢ (R Or x \land (v \in x \land y \in x)) \to (v R y \to \{w \in x \| w R v\} [\subset] \{w \in x \| w R y\})$
33		breq2	$⊢ v = y \to (w R v \leftrightarrow w R y)$
34	33	rabbidv	$⊢ v = y \to \{w \in x \| w R v\} = \{w \in x \| w R y\}$
35	34	a1i	$⊢ (R Or x \land (v \in x \land y \in x)) \to (v = y \to \{w \in x \| w R v\} = \{w \in x \| w R y\})$
36		fin2solem	$⊢ (R Or x \land (y \in x \land v \in x)) \to (y R v \to \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\})$
37	36	ancom2s	$⊢ (R Or x \land (v \in x \land y \in x)) \to (y R v \to \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\})$
38	32 35 37	3orim123d	$⊢ (R Or x \land (v \in x \land y \in x)) \to ((v R y \lor v = y \lor y R v) \to (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\}))$
39	31 38	mpd	$⊢ (R Or x \land (v \in x \land y \in x)) \to (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\})$
40	39	ralrimivva	$⊢ R Or x \to \forall v \in x \forall y \in x (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\})$
41		breq1	$⊢ u = \{w \in x \| w R v\} \to (u [\subset] \{w \in x \| w R y\} \leftrightarrow \{w \in x \| w R v\} [\subset] \{w \in x \| w R y\})$
42		eqeq1	$⊢ u = \{w \in x \| w R v\} \to (u = \{w \in x \| w R y\} \leftrightarrow \{w \in x \| w R v\} = \{w \in x \| w R y\})$
43		breq2	$⊢ u = \{w \in x \| w R v\} \to (\{w \in x \| w R y\} [\subset] u \leftrightarrow \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\})$
44	41 42 43	3orbi123d	$⊢ u = \{w \in x \| w R v\} \to ((u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u) \leftrightarrow (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\}))$
45	44	ralbidv	$⊢ u = \{w \in x \| w R v\} \to (\forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u) \leftrightarrow \forall y \in x (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\}))$
46	12 45	ralrnmptw	$⊢ \forall v \in x \{w \in x \| w R v\} \in V \to (\forall u \in ran (v \in x ⟼ \{w \in x \| w R v\}) \forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u) \leftrightarrow \forall v \in x \forall y \in x (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\}))$
47	11 46	ax-mp	$⊢ \forall u \in ran (v \in x ⟼ \{w \in x \| w R v\}) \forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u) \leftrightarrow \forall v \in x \forall y \in x (\{w \in x \| w R v\} [\subset] \{w \in x \| w R y\} \lor \{w \in x \| w R v\} = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] \{w \in x \| w R v\})$
48	40 47	sylibr	$⊢ R Or x \to \forall u \in ran (v \in x ⟼ \{w \in x \| w R v\}) \forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u)$
49	48	r19.21bi	$⊢ (R Or x \land u \in ran (v \in x ⟼ \{w \in x \| w R v\})) \to \forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u)$
50	9	rabex	$⊢ \{w \in x \| w R y\} \in V$
51	50	rgenw	$⊢ \forall y \in x \{w \in x \| w R y\} \in V$
52	34	cbvmptv	$⊢ (v \in x ⟼ \{w \in x \| w R v\}) = (y \in x ⟼ \{w \in x \| w R y\})$
53		breq2	$⊢ z = \{w \in x \| w R y\} \to (u [\subset] z \leftrightarrow u [\subset] \{w \in x \| w R y\})$
54		eqeq2	$⊢ z = \{w \in x \| w R y\} \to (u = z \leftrightarrow u = \{w \in x \| w R y\})$
55		breq1	$⊢ z = \{w \in x \| w R y\} \to (z [\subset] u \leftrightarrow \{w \in x \| w R y\} [\subset] u)$
56	53 54 55	3orbi123d	$⊢ z = \{w \in x \| w R y\} \to ((u [\subset] z \lor u = z \lor z [\subset] u) \leftrightarrow (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u))$
57	52 56	ralrnmptw	$⊢ \forall y \in x \{w \in x \| w R y\} \in V \to (\forall z \in ran (v \in x ⟼ \{w \in x \| w R v\}) (u [\subset] z \lor u = z \lor z [\subset] u) \leftrightarrow \forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u))$
58	51 57	ax-mp	$⊢ \forall z \in ran (v \in x ⟼ \{w \in x \| w R v\}) (u [\subset] z \lor u = z \lor z [\subset] u) \leftrightarrow \forall y \in x (u [\subset] \{w \in x \| w R y\} \lor u = \{w \in x \| w R y\} \lor \{w \in x \| w R y\} [\subset] u)$
59	49 58	sylibr	$⊢ (R Or x \land u \in ran (v \in x ⟼ \{w \in x \| w R v\})) \to \forall z \in ran (v \in x ⟼ \{w \in x \| w R v\}) (u [\subset] z \lor u = z \lor z [\subset] u)$
60	59	r19.21bi	$⊢ ((R Or x \land u \in ran (v \in x ⟼ \{w \in x \| w R v\})) \land z \in ran (v \in x ⟼ \{w \in x \| w R v\})) \to (u [\subset] z \lor u = z \lor z [\subset] u)$
61	60	anasss	$⊢ (R Or x \land (u \in ran (v \in x ⟼ \{w \in x \| w R v\}) \land z \in ran (v \in x ⟼ \{w \in x \| w R v\}))) \to (u [\subset] z \lor u = z \lor z [\subset] u)$
62	30 61	issod	$⊢ R Or x \to [\subset] Or ran (v \in x ⟼ \{w \in x \| w R v\})$
63	28 62	syl	$⊢ (R Or A \land x \subseteq A) \to [\subset] Or ran (v \in x ⟼ \{w \in x \| w R v\})$
64	63	adantll	$⊢ ((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \to [\subset] Or ran (v \in x ⟼ \{w \in x \| w R v\})$
65	64	adantr	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to [\subset] Or ran (v \in x ⟼ \{w \in x \| w R v\})$
66		fin2i2	$⊢ ((A \in {Fin}^{II} \land ran (v \in x ⟼ \{w \in x \| w R v\}) \subseteq 𝒫 A) \land (ran (v \in x ⟼ \{w \in x \| w R v\}) \neq \emptyset \land [\subset] Or ran (v \in x ⟼ \{w \in x \| w R v\}))) \to ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \in ran (v \in x ⟼ \{w \in x \| w R v\})$
67	1 20 26 65 66	syl22anc	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \in ran (v \in x ⟼ \{w \in x \| w R v\})$
68	52 50	elrnmpti	$⊢ ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \in ran (v \in x ⟼ \{w \in x \| w R v\}) \leftrightarrow \exists y \in x ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}$
69	67 68	sylib	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to \exists y \in x ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}$
70		ssel2	$⊢ (x \subseteq A \land z \in x) \to z \in A$
71		sonr	$⊢ (R Or A \land z \in A) \to \neg z R z$
72	70 71	sylan2	$⊢ (R Or A \land (x \subseteq A \land z \in x)) \to \neg z R z$
73	72	anassrs	$⊢ ((R Or A \land x \subseteq A) \land z \in x) \to \neg z R z$
74	73	adantlr	$⊢ (((R Or A \land x \subseteq A) \land y \in x) \land z \in x) \to \neg z R z$
75	74	adantr	$⊢ ((((R Or A \land x \subseteq A) \land y \in x) \land z \in x) \land ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}) \to \neg z R z$
76		breq1	$⊢ w = z \to (w R y \leftrightarrow z R y)$
77	76	elrab	$⊢ z \in \{w \in x \| w R y\} \leftrightarrow (z \in x \land z R y)$
78	77	simplbi2	$⊢ z \in x \to (z R y \to z \in \{w \in x \| w R y\})$
79	78	ad2antlr	$⊢ ((y \in x \land z \in x) \land ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}) \to (z R y \to z \in \{w \in x \| w R y\})$
80		vex	$⊢ z \in V$
81	80	elint2	$⊢ z \in ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \leftrightarrow \forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) z \in y$
82		eleq2	$⊢ y = \{w \in x \| w R v\} \to (z \in y \leftrightarrow z \in \{w \in x \| w R v\})$
83	12 82	ralrnmptw	$⊢ \forall v \in x \{w \in x \| w R v\} \in V \to (\forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) z \in y \leftrightarrow \forall v \in x z \in \{w \in x \| w R v\})$
84	11 83	ax-mp	$⊢ \forall y \in ran (v \in x ⟼ \{w \in x \| w R v\}) z \in y \leftrightarrow \forall v \in x z \in \{w \in x \| w R v\}$
85	81 84	bitri	$⊢ z \in ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \leftrightarrow \forall v \in x z \in \{w \in x \| w R v\}$
86		breq2	$⊢ v = z \to (w R v \leftrightarrow w R z)$
87	86	rabbidv	$⊢ v = z \to \{w \in x \| w R v\} = \{w \in x \| w R z\}$
88	87	eleq2d	$⊢ v = z \to (z \in \{w \in x \| w R v\} \leftrightarrow z \in \{w \in x \| w R z\})$
89	88	rspcv	$⊢ z \in x \to (\forall v \in x z \in \{w \in x \| w R v\} \to z \in \{w \in x \| w R z\})$
90		breq1	$⊢ w = z \to (w R z \leftrightarrow z R z)$
91	90	elrab	$⊢ z \in \{w \in x \| w R z\} \leftrightarrow (z \in x \land z R z)$
92	91	simprbi	$⊢ z \in \{w \in x \| w R z\} \to z R z$
93	89 92	syl6	$⊢ z \in x \to (\forall v \in x z \in \{w \in x \| w R v\} \to z R z)$
94	93	adantl	$⊢ (y \in x \land z \in x) \to (\forall v \in x z \in \{w \in x \| w R v\} \to z R z)$
95	85 94	syl5bi	$⊢ (y \in x \land z \in x) \to (z \in ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \to z R z)$
96		eleq2	$⊢ ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to (z \in ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \leftrightarrow z \in \{w \in x \| w R y\})$
97	96	imbi1d	$⊢ ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to ((z \in ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) \to z R z) \leftrightarrow (z \in \{w \in x \| w R y\} \to z R z))$
98	95 97	syl5ibcom	$⊢ (y \in x \land z \in x) \to (⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to (z \in \{w \in x \| w R y\} \to z R z))$
99	98	imp	$⊢ ((y \in x \land z \in x) \land ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}) \to (z \in \{w \in x \| w R y\} \to z R z)$
100	79 99	syld	$⊢ ((y \in x \land z \in x) \land ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}) \to (z R y \to z R z)$
101	100	adantlll	$⊢ ((((R Or A \land x \subseteq A) \land y \in x) \land z \in x) \land ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}) \to (z R y \to z R z)$
102	75 101	mtod	$⊢ ((((R Or A \land x \subseteq A) \land y \in x) \land z \in x) \land ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\}) \to \neg z R y$
103	102	ex	$⊢ (((R Or A \land x \subseteq A) \land y \in x) \land z \in x) \to (⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to \neg z R y)$
104	103	ralrimdva	$⊢ ((R Or A \land x \subseteq A) \land y \in x) \to (⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to \forall z \in x \neg z R y)$
105	104	reximdva	$⊢ (R Or A \land x \subseteq A) \to (\exists y \in x ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to \exists y \in x \forall z \in x \neg z R y)$
106	105	adantll	$⊢ ((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \to (\exists y \in x ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to \exists y \in x \forall z \in x \neg z R y)$
107	106	adantr	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to (\exists y \in x ⋂ ran (v \in x ⟼ \{w \in x \| w R v\}) = \{w \in x \| w R y\} \to \exists y \in x \forall z \in x \neg z R y)$
108	69 107	mpd	$⊢ (((A \in {Fin}^{II} \land R Or A) \land x \subseteq A) \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y$
109	108	expl	$⊢ (A \in {Fin}^{II} \land R Or A) \to ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
110	109	alrimiv	$⊢ (A \in {Fin}^{II} \land R Or A) \to \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
111		df-fr	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
112	110 111	sylibr	$⊢ (A \in {Fin}^{II} \land R Or A) \to R Fr A$
113		simpr	$⊢ (A \in {Fin}^{II} \land R Or A) \to R Or A$
114		df-we	$⊢ R We A \leftrightarrow (R Fr A \land R Or A)$
115	112 113 114	sylanbrc	$⊢ (A \in {Fin}^{II} \land R Or A) \to R We A$
116		weinxp	$⊢ R We A \leftrightarrow (R \cap (A \times A)) We A$
117	115 116	sylib	$⊢ (A \in {Fin}^{II} \land R Or A) \to (R \cap (A \times A)) We A$
118		sqxpexg	$⊢ A \in {Fin}^{II} \to A \times A \in V$
119		incom	$⊢ R \cap (A \times A) = (A \times A) \cap R$
120		inex1g	$⊢ A \times A \in V \to (A \times A) \cap R \in V$
121	119 120	eqeltrid	$⊢ A \times A \in V \to R \cap (A \times A) \in V$
122		weeq1	$⊢ z = R \cap (A \times A) \to (z We A \leftrightarrow (R \cap (A \times A)) We A)$
123	122	spcegv	$⊢ R \cap (A \times A) \in V \to ((R \cap (A \times A)) We A \to \exists z z We A)$
124	118 121 123	3syl	$⊢ A \in {Fin}^{II} \to ((R \cap (A \times A)) We A \to \exists z z We A)$
125	124	imp	$⊢ (A \in {Fin}^{II} \land (R \cap (A \times A)) We A) \to \exists z z We A$
126	117 125	syldan	$⊢ (A \in {Fin}^{II} \land R Or A) \to \exists z z We A$
127		ween	$⊢ A \in dom card \leftrightarrow \exists z z We A$
128	126 127	sylibr	$⊢ (A \in {Fin}^{II} \land R Or A) \to A \in dom card$
129		fin23	$⊢ A \in {Fin}^{II} \to A \in {Fin}^{III}$
130		fin34	$⊢ A \in {Fin}^{III} \to A \in {Fin}^{IV}$
131		fin45	$⊢ A \in {Fin}^{IV} \to A \in {Fin}^{V}$
132	129 130 131	3syl	$⊢ A \in {Fin}^{II} \to A \in {Fin}^{V}$
133		fin56	$⊢ A \in {Fin}^{V} \to A \in {Fin}^{VI}$
134		fin67	$⊢ A \in {Fin}^{VI} \to A \in {Fin}^{VII}$
135	132 133 134	3syl	$⊢ A \in {Fin}^{II} \to A \in {Fin}^{VII}$
136		fin71num	$⊢ A \in dom card \to (A \in {Fin}^{VII} \leftrightarrow A \in Fin)$
137	136	biimpac	$⊢ (A \in {Fin}^{VII} \land A \in dom card) \to A \in Fin$
138	135 137	sylan	$⊢ (A \in {Fin}^{II} \land A \in dom card) \to A \in Fin$
139	128 138	syldan	$⊢ (A \in {Fin}^{II} \land R Or A) \to A \in Fin$

Metamath Proof Explorer

Theorem fin2so

Proof