fin23lem40

Description: Lemma for fin23 . Fin2 sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014)

		Ref	Expression
	Hypothesis	fin23lem40.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	Assertion	fin23lem40	$⊢ A \in {Fin}^{II} \to A \in F$

Proof

Step	Hyp	Ref	Expression
1		fin23lem40.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
2		elmapi	$⊢ f \in ({𝒫 A}^{ω}) \to f : ω ⟶ 𝒫 A$
3		simpl	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to A \in {Fin}^{II}$
4		frn	$⊢ f : ω ⟶ 𝒫 A \to ran f \subseteq 𝒫 A$
5	4	ad2antrl	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to ran f \subseteq 𝒫 A$
6		fdm	$⊢ f : ω ⟶ 𝒫 A \to dom f = ω$
7		peano1	$⊢ \emptyset \in ω$
8		ne0i	$⊢ \emptyset \in ω \to ω \neq \emptyset$
9	7 8	mp1i	$⊢ f : ω ⟶ 𝒫 A \to ω \neq \emptyset$
10	6 9	eqnetrd	$⊢ f : ω ⟶ 𝒫 A \to dom f \neq \emptyset$
11		dm0rn0	$⊢ dom f = \emptyset \leftrightarrow ran f = \emptyset$
12	11	necon3bii	$⊢ dom f \neq \emptyset \leftrightarrow ran f \neq \emptyset$
13	10 12	sylib	$⊢ f : ω ⟶ 𝒫 A \to ran f \neq \emptyset$
14	13	ad2antrl	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to ran f \neq \emptyset$
15		ffn	$⊢ f : ω ⟶ 𝒫 A \to f Fn ω$
16	15	ad2antrl	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to f Fn ω$
17		sspss	$⊢ f (suc b) \subseteq f (b) \leftrightarrow (f (suc b) \subset f (b) \lor f (suc b) = f (b))$
18		fvex	$⊢ f (b) \in V$
19		fvex	$⊢ f (suc b) \in V$
20	18 19	brcnv	$⊢ f (b) {[\subset]}^{-1} f (suc b) \leftrightarrow f (suc b) [\subset] f (b)$
21	18	brrpss	$⊢ f (suc b) [\subset] f (b) \leftrightarrow f (suc b) \subset f (b)$
22	20 21	bitri	$⊢ f (b) {[\subset]}^{-1} f (suc b) \leftrightarrow f (suc b) \subset f (b)$
23		eqcom	$⊢ f (b) = f (suc b) \leftrightarrow f (suc b) = f (b)$
24	22 23	orbi12i	$⊢ (f (b) {[\subset]}^{-1} f (suc b) \lor f (b) = f (suc b)) \leftrightarrow (f (suc b) \subset f (b) \lor f (suc b) = f (b))$
25	17 24	sylbb2	$⊢ f (suc b) \subseteq f (b) \to (f (b) {[\subset]}^{-1} f (suc b) \lor f (b) = f (suc b))$
26	25	ralimi	$⊢ \forall b \in ω f (suc b) \subseteq f (b) \to \forall b \in ω (f (b) {[\subset]}^{-1} f (suc b) \lor f (b) = f (suc b))$
27	26	ad2antll	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to \forall b \in ω (f (b) {[\subset]}^{-1} f (suc b) \lor f (b) = f (suc b))$
28		porpss	$⊢ [\subset] Po ran f$
29		cnvpo	$⊢ [\subset] Po ran f \leftrightarrow {[\subset]}^{-1} Po ran f$
30	28 29	mpbi	$⊢ {[\subset]}^{-1} Po ran f$
31	30	a1i	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to {[\subset]}^{-1} Po ran f$
32		sornom	$⊢ (f Fn ω \land \forall b \in ω (f (b) {[\subset]}^{-1} f (suc b) \lor f (b) = f (suc b)) \land {[\subset]}^{-1} Po ran f) \to {[\subset]}^{-1} Or ran f$
33	16 27 31 32	syl3anc	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to {[\subset]}^{-1} Or ran f$
34		cnvso	$⊢ [\subset] Or ran f \leftrightarrow {[\subset]}^{-1} Or ran f$
35	33 34	sylibr	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to [\subset] Or ran f$
36		fin2i2	$⊢ ((A \in {Fin}^{II} \land ran f \subseteq 𝒫 A) \land (ran f \neq \emptyset \land [\subset] Or ran f)) \to ⋂ ran f \in ran f$
37	3 5 14 35 36	syl22anc	$⊢ (A \in {Fin}^{II} \land (f : ω ⟶ 𝒫 A \land \forall b \in ω f (suc b) \subseteq f (b))) \to ⋂ ran f \in ran f$
38	37	expr	$⊢ (A \in {Fin}^{II} \land f : ω ⟶ 𝒫 A) \to (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f)$
39	2 38	sylan2	$⊢ (A \in {Fin}^{II} \land f \in ({𝒫 A}^{ω})) \to (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f)$
40	39	ralrimiva	$⊢ A \in {Fin}^{II} \to \forall f \in ({𝒫 A}^{ω}) (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f)$
41	1	isfin3ds	$⊢ A \in {Fin}^{II} \to (A \in F \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall b \in ω f (suc b) \subseteq f (b) \to ⋂ ran f \in ran f))$
42	40 41	mpbird	$⊢ A \in {Fin}^{II} \to A \in F$

Metamath Proof Explorer

Theorem fin23lem40

Proof