isfin1-3

Description: A set is I-finite iff every system of subsets contains a maximal subset. Definition I of Levy58 p. 2. (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	isfin1-3	$⊢ A \in V \to (A \in Fin \leftrightarrow {[\subset]}^{-1} Fr 𝒫 A)$

Proof

Step	Hyp	Ref	Expression
1		porpss	$⊢ [\subset] Po 𝒫 A$
2		cnvpo	$⊢ [\subset] Po 𝒫 A \leftrightarrow {[\subset]}^{-1} Po 𝒫 A$
3	1 2	mpbi	$⊢ {[\subset]}^{-1} Po 𝒫 A$
4		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
5	4	biimpi	$⊢ A \in Fin \to 𝒫 A \in Fin$
6		frfi	$⊢ ({[\subset]}^{-1} Po 𝒫 A \land 𝒫 A \in Fin) \to {[\subset]}^{-1} Fr 𝒫 A$
7	3 5 6	sylancr	$⊢ A \in Fin \to {[\subset]}^{-1} Fr 𝒫 A$
8		inss2	$⊢ Fin \cap 𝒫 A \subseteq 𝒫 A$
9		pwexg	$⊢ A \in V \to 𝒫 A \in V$
10		ssexg	$⊢ (Fin \cap 𝒫 A \subseteq 𝒫 A \land 𝒫 A \in V) \to Fin \cap 𝒫 A \in V$
11	8 9 10	sylancr	$⊢ A \in V \to Fin \cap 𝒫 A \in V$
12		0fin	$⊢ \emptyset \in Fin$
13		0elpw	$⊢ \emptyset \in 𝒫 A$
14	12 13	elini	$⊢ \emptyset \in (Fin \cap 𝒫 A)$
15	14	ne0ii	$⊢ Fin \cap 𝒫 A \neq \emptyset$
16		fri	$⊢ ((Fin \cap 𝒫 A \in V \land {[\subset]}^{-1} Fr 𝒫 A) \land (Fin \cap 𝒫 A \subseteq 𝒫 A \land Fin \cap 𝒫 A \neq \emptyset)) \to \exists b \in (Fin \cap 𝒫 A) \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b$
17	8 15 16	mpanr12	$⊢ (Fin \cap 𝒫 A \in V \land {[\subset]}^{-1} Fr 𝒫 A) \to \exists b \in (Fin \cap 𝒫 A) \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b$
18	11 17	sylan	$⊢ (A \in V \land {[\subset]}^{-1} Fr 𝒫 A) \to \exists b \in (Fin \cap 𝒫 A) \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b$
19	18	ex	$⊢ A \in V \to ({[\subset]}^{-1} Fr 𝒫 A \to \exists b \in (Fin \cap 𝒫 A) \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b)$
20		elinel1	$⊢ b \in (Fin \cap 𝒫 A) \to b \in Fin$
21		ralnex	$⊢ \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b \leftrightarrow \neg \exists c \in (Fin \cap 𝒫 A) c {[\subset]}^{-1} b$
22	20	adantr	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \in Fin$
23		snfi	$⊢ \{d\} \in Fin$
24		unfi	$⊢ (b \in Fin \land \{d\} \in Fin) \to b \cup \{d\} \in Fin$
25	22 23 24	sylancl	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \cup \{d\} \in Fin$
26		elinel2	$⊢ b \in (Fin \cap 𝒫 A) \to b \in 𝒫 A$
27	26	elpwid	$⊢ b \in (Fin \cap 𝒫 A) \to b \subseteq A$
28	27	adantr	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \subseteq A$
29		snssi	$⊢ d \in A \to \{d\} \subseteq A$
30	29	ad2antrl	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to \{d\} \subseteq A$
31	28 30	unssd	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \cup \{d\} \subseteq A$
32		vex	$⊢ b \in V$
33		snex	$⊢ \{d\} \in V$
34	32 33	unex	$⊢ b \cup \{d\} \in V$
35	34	elpw	$⊢ b \cup \{d\} \in 𝒫 A \leftrightarrow b \cup \{d\} \subseteq A$
36	31 35	sylibr	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \cup \{d\} \in 𝒫 A$
37	25 36	elind	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \cup \{d\} \in (Fin \cap 𝒫 A)$
38		disjsn	$⊢ b \cap \{d\} = \emptyset \leftrightarrow \neg d \in b$
39	38	biimpri	$⊢ \neg d \in b \to b \cap \{d\} = \emptyset$
40		vex	$⊢ d \in V$
41	40	snnz	$⊢ \{d\} \neq \emptyset$
42		disjpss	$⊢ (b \cap \{d\} = \emptyset \land \{d\} \neq \emptyset) \to b \subset b \cup \{d\}$
43	39 41 42	sylancl	$⊢ \neg d \in b \to b \subset b \cup \{d\}$
44	43	ad2antll	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to b \subset b \cup \{d\}$
45	34 32	brcnv	$⊢ (b \cup \{d\}) {[\subset]}^{-1} b \leftrightarrow b [\subset] (b \cup \{d\})$
46	34	brrpss	$⊢ b [\subset] (b \cup \{d\}) \leftrightarrow b \subset b \cup \{d\}$
47	45 46	bitri	$⊢ (b \cup \{d\}) {[\subset]}^{-1} b \leftrightarrow b \subset b \cup \{d\}$
48	44 47	sylibr	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to (b \cup \{d\}) {[\subset]}^{-1} b$
49		breq1	$⊢ c = b \cup \{d\} \to (c {[\subset]}^{-1} b \leftrightarrow (b \cup \{d\}) {[\subset]}^{-1} b)$
50	49	rspcev	$⊢ (b \cup \{d\} \in (Fin \cap 𝒫 A) \land (b \cup \{d\}) {[\subset]}^{-1} b) \to \exists c \in (Fin \cap 𝒫 A) c {[\subset]}^{-1} b$
51	37 48 50	syl2anc	$⊢ (b \in (Fin \cap 𝒫 A) \land (d \in A \land \neg d \in b)) \to \exists c \in (Fin \cap 𝒫 A) c {[\subset]}^{-1} b$
52	51	expr	$⊢ (b \in (Fin \cap 𝒫 A) \land d \in A) \to (\neg d \in b \to \exists c \in (Fin \cap 𝒫 A) c {[\subset]}^{-1} b)$
53	52	con1d	$⊢ (b \in (Fin \cap 𝒫 A) \land d \in A) \to (\neg \exists c \in (Fin \cap 𝒫 A) c {[\subset]}^{-1} b \to d \in b)$
54	21 53	syl5bi	$⊢ (b \in (Fin \cap 𝒫 A) \land d \in A) \to (\forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b \to d \in b)$
55	54	impancom	$⊢ (b \in (Fin \cap 𝒫 A) \land \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b) \to (d \in A \to d \in b)$
56	55	ssrdv	$⊢ (b \in (Fin \cap 𝒫 A) \land \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b) \to A \subseteq b$
57		ssfi	$⊢ (b \in Fin \land A \subseteq b) \to A \in Fin$
58	20 56 57	syl2an2r	$⊢ (b \in (Fin \cap 𝒫 A) \land \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b) \to A \in Fin$
59	58	rexlimiva	$⊢ \exists b \in (Fin \cap 𝒫 A) \forall c \in (Fin \cap 𝒫 A) \neg c {[\subset]}^{-1} b \to A \in Fin$
60	19 59	syl6	$⊢ A \in V \to ({[\subset]}^{-1} Fr 𝒫 A \to A \in Fin)$
61	7 60	impbid2	$⊢ A \in V \to (A \in Fin \leftrightarrow {[\subset]}^{-1} Fr 𝒫 A)$

Metamath Proof Explorer

Theorem isfin1-3

Proof