isf34lem6

		Ref	Expression
	Hypothesis	compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
	Assertion	isf34lem6	$⊢ A \in V \to (A \in {Fin}^{III} \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f))$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
2		elmapi	$⊢ f \in ({𝒫 A}^{ω}) \to f : ω ⟶ 𝒫 A$
3	1	isf34lem7	$⊢ (A \in {Fin}^{III} \land f : ω ⟶ 𝒫 A \land \forall y \in ω f (y) \subseteq f (suc y)) \to ⋃ ran f \in ran f$
4	3	3expia	$⊢ (A \in {Fin}^{III} \land f : ω ⟶ 𝒫 A) \to (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f)$
5	2 4	sylan2	$⊢ (A \in {Fin}^{III} \land f \in ({𝒫 A}^{ω})) \to (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f)$
6	5	ralrimiva	$⊢ A \in {Fin}^{III} \to \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f)$
7		elmapex	$⊢ g \in ({𝒫 A}^{ω}) \to (𝒫 A \in V \land ω \in V)$
8	7	simpld	$⊢ g \in ({𝒫 A}^{ω}) \to 𝒫 A \in V$
9		pwexb	$⊢ A \in V \leftrightarrow 𝒫 A \in V$
10	8 9	sylibr	$⊢ g \in ({𝒫 A}^{ω}) \to A \in V$
11	1	isf34lem2	$⊢ A \in V \to F : 𝒫 A ⟶ 𝒫 A$
12	10 11	syl	$⊢ g \in ({𝒫 A}^{ω}) \to F : 𝒫 A ⟶ 𝒫 A$
13		elmapi	$⊢ g \in ({𝒫 A}^{ω}) \to g : ω ⟶ 𝒫 A$
14		fco	$⊢ (F : 𝒫 A ⟶ 𝒫 A \land g : ω ⟶ 𝒫 A) \to (F \circ g) : ω ⟶ 𝒫 A$
15	12 13 14	syl2anc	$⊢ g \in ({𝒫 A}^{ω}) \to (F \circ g) : ω ⟶ 𝒫 A$
16		elmapg	$⊢ (𝒫 A \in V \land ω \in V) \to (F \circ g \in ({𝒫 A}^{ω}) \leftrightarrow (F \circ g) : ω ⟶ 𝒫 A)$
17	7 16	syl	$⊢ g \in ({𝒫 A}^{ω}) \to (F \circ g \in ({𝒫 A}^{ω}) \leftrightarrow (F \circ g) : ω ⟶ 𝒫 A)$
18	15 17	mpbird	$⊢ g \in ({𝒫 A}^{ω}) \to F \circ g \in ({𝒫 A}^{ω})$
19		fveq1	$⊢ f = F \circ g \to f (y) = (F \circ g) (y)$
20		fveq1	$⊢ f = F \circ g \to f (suc y) = (F \circ g) (suc y)$
21	19 20	sseq12d	$⊢ f = F \circ g \to (f (y) \subseteq f (suc y) \leftrightarrow (F \circ g) (y) \subseteq (F \circ g) (suc y))$
22	21	ralbidv	$⊢ f = F \circ g \to (\forall y \in ω f (y) \subseteq f (suc y) \leftrightarrow \forall y \in ω (F \circ g) (y) \subseteq (F \circ g) (suc y))$
23		rneq	$⊢ f = F \circ g \to ran f = ran (F \circ g)$
24		rnco2	$⊢ ran (F \circ g) = F [ran g]$
25	23 24	eqtrdi	$⊢ f = F \circ g \to ran f = F [ran g]$
26	25	unieqd	$⊢ f = F \circ g \to ⋃ ran f = ⋃ F [ran g]$
27	26 25	eleq12d	$⊢ f = F \circ g \to (⋃ ran f \in ran f \leftrightarrow ⋃ F [ran g] \in F [ran g])$
28	22 27	imbi12d	$⊢ f = F \circ g \to ((\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f) \leftrightarrow (\forall y \in ω (F \circ g) (y) \subseteq (F \circ g) (suc y) \to ⋃ F [ran g] \in F [ran g]))$
29	28	rspccv	$⊢ \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f) \to (F \circ g \in ({𝒫 A}^{ω}) \to (\forall y \in ω (F \circ g) (y) \subseteq (F \circ g) (suc y) \to ⋃ F [ran g] \in F [ran g]))$
30	18 29	syl5	$⊢ \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f) \to (g \in ({𝒫 A}^{ω}) \to (\forall y \in ω (F \circ g) (y) \subseteq (F \circ g) (suc y) \to ⋃ F [ran g] \in F [ran g]))$
31		sscon	$⊢ g (suc y) \subseteq g (y) \to A ∖ g (y) \subseteq A ∖ g (suc y)$
32	13	ffvelcdmda	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to g (y) \in 𝒫 A$
33	32	elpwid	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to g (y) \subseteq A$
34	1	isf34lem1	$⊢ (A \in V \land g (y) \subseteq A) \to F (g (y)) = A ∖ g (y)$
35	10 33 34	syl2an2r	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to F (g (y)) = A ∖ g (y)$
36		peano2	$⊢ y \in ω \to suc y \in ω$
37		ffvelcdm	$⊢ (g : ω ⟶ 𝒫 A \land suc y \in ω) \to g (suc y) \in 𝒫 A$
38	13 36 37	syl2an	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to g (suc y) \in 𝒫 A$
39	38	elpwid	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to g (suc y) \subseteq A$
40	1	isf34lem1	$⊢ (A \in V \land g (suc y) \subseteq A) \to F (g (suc y)) = A ∖ g (suc y)$
41	10 39 40	syl2an2r	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to F (g (suc y)) = A ∖ g (suc y)$
42	35 41	sseq12d	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to (F (g (y)) \subseteq F (g (suc y)) \leftrightarrow A ∖ g (y) \subseteq A ∖ g (suc y))$
43	31 42	imbitrrid	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to (g (suc y) \subseteq g (y) \to F (g (y)) \subseteq F (g (suc y)))$
44		fvco3	$⊢ (g : ω ⟶ 𝒫 A \land y \in ω) \to (F \circ g) (y) = F (g (y))$
45	13 44	sylan	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to (F \circ g) (y) = F (g (y))$
46		fvco3	$⊢ (g : ω ⟶ 𝒫 A \land suc y \in ω) \to (F \circ g) (suc y) = F (g (suc y))$
47	13 36 46	syl2an	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to (F \circ g) (suc y) = F (g (suc y))$
48	45 47	sseq12d	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to ((F \circ g) (y) \subseteq (F \circ g) (suc y) \leftrightarrow F (g (y)) \subseteq F (g (suc y)))$
49	43 48	sylibrd	$⊢ (g \in ({𝒫 A}^{ω}) \land y \in ω) \to (g (suc y) \subseteq g (y) \to (F \circ g) (y) \subseteq (F \circ g) (suc y))$
50	49	ralimdva	$⊢ g \in ({𝒫 A}^{ω}) \to (\forall y \in ω g (suc y) \subseteq g (y) \to \forall y \in ω (F \circ g) (y) \subseteq (F \circ g) (suc y))$
51	12	ffnd	$⊢ g \in ({𝒫 A}^{ω}) \to F Fn 𝒫 A$
52		imassrn	$⊢ F [ran g] \subseteq ran F$
53	12	frnd	$⊢ g \in ({𝒫 A}^{ω}) \to ran F \subseteq 𝒫 A$
54	52 53	sstrid	$⊢ g \in ({𝒫 A}^{ω}) \to F [ran g] \subseteq 𝒫 A$
55		fnfvima	$⊢ (F Fn 𝒫 A \land F [ran g] \subseteq 𝒫 A \land ⋃ F [ran g] \in F [ran g]) \to F (⋃ F [ran g]) \in F [F [ran g]]$
56	55	3expia	$⊢ (F Fn 𝒫 A \land F [ran g] \subseteq 𝒫 A) \to (⋃ F [ran g] \in F [ran g] \to F (⋃ F [ran g]) \in F [F [ran g]])$
57	51 54 56	syl2anc	$⊢ g \in ({𝒫 A}^{ω}) \to (⋃ F [ran g] \in F [ran g] \to F (⋃ F [ran g]) \in F [F [ran g]])$
58		incom	$⊢ dom F \cap ran g = ran g \cap dom F$
59	13	frnd	$⊢ g \in ({𝒫 A}^{ω}) \to ran g \subseteq 𝒫 A$
60	12	fdmd	$⊢ g \in ({𝒫 A}^{ω}) \to dom F = 𝒫 A$
61	59 60	sseqtrrd	$⊢ g \in ({𝒫 A}^{ω}) \to ran g \subseteq dom F$
62		df-ss	$⊢ ran g \subseteq dom F \leftrightarrow ran g \cap dom F = ran g$
63	61 62	sylib	$⊢ g \in ({𝒫 A}^{ω}) \to ran g \cap dom F = ran g$
64	58 63	eqtrid	$⊢ g \in ({𝒫 A}^{ω}) \to dom F \cap ran g = ran g$
65	13	fdmd	$⊢ g \in ({𝒫 A}^{ω}) \to dom g = ω$
66		peano1	$⊢ \emptyset \in ω$
67		ne0i	$⊢ \emptyset \in ω \to ω \neq \emptyset$
68	66 67	mp1i	$⊢ g \in ({𝒫 A}^{ω}) \to ω \neq \emptyset$
69	65 68	eqnetrd	$⊢ g \in ({𝒫 A}^{ω}) \to dom g \neq \emptyset$
70		dm0rn0	$⊢ dom g = \emptyset \leftrightarrow ran g = \emptyset$
71	70	necon3bii	$⊢ dom g \neq \emptyset \leftrightarrow ran g \neq \emptyset$
72	69 71	sylib	$⊢ g \in ({𝒫 A}^{ω}) \to ran g \neq \emptyset$
73	64 72	eqnetrd	$⊢ g \in ({𝒫 A}^{ω}) \to dom F \cap ran g \neq \emptyset$
74		imadisj	$⊢ F [ran g] = \emptyset \leftrightarrow dom F \cap ran g = \emptyset$
75	74	necon3bii	$⊢ F [ran g] \neq \emptyset \leftrightarrow dom F \cap ran g \neq \emptyset$
76	73 75	sylibr	$⊢ g \in ({𝒫 A}^{ω}) \to F [ran g] \neq \emptyset$
77	1	isf34lem4	$⊢ (A \in V \land (F [ran g] \subseteq 𝒫 A \land F [ran g] \neq \emptyset)) \to F (⋃ F [ran g]) = ⋂ F [F [ran g]]$
78	10 54 76 77	syl12anc	$⊢ g \in ({𝒫 A}^{ω}) \to F (⋃ F [ran g]) = ⋂ F [F [ran g]]$
79	1	isf34lem3	$⊢ (A \in V \land ran g \subseteq 𝒫 A) \to F [F [ran g]] = ran g$
80	10 59 79	syl2anc	$⊢ g \in ({𝒫 A}^{ω}) \to F [F [ran g]] = ran g$
81	80	inteqd	$⊢ g \in ({𝒫 A}^{ω}) \to ⋂ F [F [ran g]] = ⋂ ran g$
82	78 81	eqtrd	$⊢ g \in ({𝒫 A}^{ω}) \to F (⋃ F [ran g]) = ⋂ ran g$
83	82 80	eleq12d	$⊢ g \in ({𝒫 A}^{ω}) \to (F (⋃ F [ran g]) \in F [F [ran g]] \leftrightarrow ⋂ ran g \in ran g)$
84	57 83	sylibd	$⊢ g \in ({𝒫 A}^{ω}) \to (⋃ F [ran g] \in F [ran g] \to ⋂ ran g \in ran g)$
85	50 84	imim12d	$⊢ g \in ({𝒫 A}^{ω}) \to ((\forall y \in ω (F \circ g) (y) \subseteq (F \circ g) (suc y) \to ⋃ F [ran g] \in F [ran g]) \to (\forall y \in ω g (suc y) \subseteq g (y) \to ⋂ ran g \in ran g))$
86	30 85	sylcom	$⊢ \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f) \to (g \in ({𝒫 A}^{ω}) \to (\forall y \in ω g (suc y) \subseteq g (y) \to ⋂ ran g \in ran g))$
87	86	ralrimiv	$⊢ \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f) \to \forall g \in ({𝒫 A}^{ω}) (\forall y \in ω g (suc y) \subseteq g (y) \to ⋂ ran g \in ran g)$
88		isfin3-3	$⊢ A \in V \to (A \in {Fin}^{III} \leftrightarrow \forall g \in ({𝒫 A}^{ω}) (\forall y \in ω g (suc y) \subseteq g (y) \to ⋂ ran g \in ran g))$
89	87 88	imbitrrid	$⊢ A \in V \to (\forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f) \to A \in {Fin}^{III})$
90	6 89	impbid2	$⊢ A \in V \to (A \in {Fin}^{III} \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall y \in ω f (y) \subseteq f (suc y) \to ⋃ ran f \in ran f))$

Metamath Proof Explorer

Theorem isf34lem6

Proof