fin23lem41

Description: Lemma for fin23 . A set which satisfies the descending sequence condition must be III-finite. (Contributed by Stefan O'Rear, 2-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	fin23lem41	$⊢ A \in F \to A \in {Fin}^{III}$

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		brdomi	$⊢ ω ≼ 𝒫 A \to \exists b b : ω \underset{1-1}{⟶} 𝒫 A$
3	1	fin23lem33	$⊢ A \in F \to \exists c \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d))$
4	3	adantl	$⊢ (b : ω \underset{1-1}{⟶} 𝒫 A \land A \in F) \to \exists c \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d))$
5		ssv	$⊢ 𝒫 A \subseteq V$
6		f1ss	$⊢ (b : ω \underset{1-1}{⟶} 𝒫 A \land 𝒫 A \subseteq V) \to b : ω \underset{1-1}{⟶} V$
7	5 6	mpan2	$⊢ b : ω \underset{1-1}{⟶} 𝒫 A \to b : ω \underset{1-1}{⟶} V$
8	7	ad2antrr	$⊢ ((b : ω \underset{1-1}{⟶} 𝒫 A \land A \in F) \land \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d))) \to b : ω \underset{1-1}{⟶} V$
9		f1f	$⊢ b : ω \underset{1-1}{⟶} 𝒫 A \to b : ω ⟶ 𝒫 A$
10		frn	$⊢ b : ω ⟶ 𝒫 A \to ran b \subseteq 𝒫 A$
11		uniss	$⊢ ran b \subseteq 𝒫 A \to ⋃ ran b \subseteq ⋃ 𝒫 A$
12	9 10 11	3syl	$⊢ b : ω \underset{1-1}{⟶} 𝒫 A \to ⋃ ran b \subseteq ⋃ 𝒫 A$
13		unipw	$⊢ ⋃ 𝒫 A = A$
14	12 13	sseqtrdi	$⊢ b : ω \underset{1-1}{⟶} 𝒫 A \to ⋃ ran b \subseteq A$
15	14	ad2antrr	$⊢ ((b : ω \underset{1-1}{⟶} 𝒫 A \land A \in F) \land \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d))) \to ⋃ ran b \subseteq A$
16		f1eq1	$⊢ d = e \to (d : ω \underset{1-1}{⟶} V \leftrightarrow e : ω \underset{1-1}{⟶} V)$
17		rneq	$⊢ d = e \to ran d = ran e$
18	17	unieqd	$⊢ d = e \to ⋃ ran d = ⋃ ran e$
19	18	sseq1d	$⊢ d = e \to (⋃ ran d \subseteq A \leftrightarrow ⋃ ran e \subseteq A)$
20	16 19	anbi12d	$⊢ d = e \to ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \leftrightarrow (e : ω \underset{1-1}{⟶} V \land ⋃ ran e \subseteq A))$
21		fveq2	$⊢ d = e \to c (d) = c (e)$
22		f1eq1	$⊢ c (d) = c (e) \to (c (d) : ω \underset{1-1}{⟶} V \leftrightarrow c (e) : ω \underset{1-1}{⟶} V)$
23	21 22	syl	$⊢ d = e \to (c (d) : ω \underset{1-1}{⟶} V \leftrightarrow c (e) : ω \underset{1-1}{⟶} V)$
24	21	rneqd	$⊢ d = e \to ran c (d) = ran c (e)$
25	24	unieqd	$⊢ d = e \to ⋃ ran c (d) = ⋃ ran c (e)$
26	25 18	psseq12d	$⊢ d = e \to (⋃ ran c (d) \subset ⋃ ran d \leftrightarrow ⋃ ran c (e) \subset ⋃ ran e)$
27	23 26	anbi12d	$⊢ d = e \to ((c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d) \leftrightarrow (c (e) : ω \underset{1-1}{⟶} V \land ⋃ ran c (e) \subset ⋃ ran e))$
28	20 27	imbi12d	$⊢ d = e \to (((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d)) \leftrightarrow ((e : ω \underset{1-1}{⟶} V \land ⋃ ran e \subseteq A) \to (c (e) : ω \underset{1-1}{⟶} V \land ⋃ ran c (e) \subset ⋃ ran e)))$
29	28	cbvalvw	$⊢ \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d)) \leftrightarrow \forall e ((e : ω \underset{1-1}{⟶} V \land ⋃ ran e \subseteq A) \to (c (e) : ω \underset{1-1}{⟶} V \land ⋃ ran c (e) \subset ⋃ ran e))$
30	29	biimpi	$⊢ \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d)) \to \forall e ((e : ω \underset{1-1}{⟶} V \land ⋃ ran e \subseteq A) \to (c (e) : ω \underset{1-1}{⟶} V \land ⋃ ran c (e) \subset ⋃ ran e))$
31	30	adantl	$⊢ ((b : ω \underset{1-1}{⟶} 𝒫 A \land A \in F) \land \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d))) \to \forall e ((e : ω \underset{1-1}{⟶} V \land ⋃ ran e \subseteq A) \to (c (e) : ω \underset{1-1}{⟶} V \land ⋃ ran c (e) \subset ⋃ ran e))$
32		eqid	$⊢ {rec (c, b) ↾}_{ω} = {rec (c, b) ↾}_{ω}$
33	1 8 15 31 32	fin23lem39	$⊢ ((b : ω \underset{1-1}{⟶} 𝒫 A \land A \in F) \land \forall d ((d : ω \underset{1-1}{⟶} V \land ⋃ ran d \subseteq A) \to (c (d) : ω \underset{1-1}{⟶} V \land ⋃ ran c (d) \subset ⋃ ran d))) \to \neg A \in F$
34	4 33	exlimddv	$⊢ (b : ω \underset{1-1}{⟶} 𝒫 A \land A \in F) \to \neg A \in F$
35	34	pm2.01da	$⊢ b : ω \underset{1-1}{⟶} 𝒫 A \to \neg A \in F$
36	35	exlimiv	$⊢ \exists b b : ω \underset{1-1}{⟶} 𝒫 A \to \neg A \in F$
37	2 36	syl	$⊢ ω ≼ 𝒫 A \to \neg A \in F$
38	37	con2i	$⊢ A \in F \to \neg ω ≼ 𝒫 A$
39		pwexg	$⊢ A \in F \to 𝒫 A \in V$
40		isfin4-2	$⊢ 𝒫 A \in V \to (𝒫 A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ 𝒫 A)$
41	39 40	syl	$⊢ A \in F \to (𝒫 A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ 𝒫 A)$
42	38 41	mpbird	$⊢ A \in F \to 𝒫 A \in {Fin}^{IV}$
43		isfin3	$⊢ A \in {Fin}^{III} \leftrightarrow 𝒫 A \in {Fin}^{IV}$
44	42 43	sylibr	$⊢ A \in F \to A \in {Fin}^{III}$

Metamath Proof Explorer

Theorem fin23lem41

Proof