isf34lem7

		Ref	Expression
	Hypothesis	compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
	Assertion	isf34lem7	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to ⋃ ran G \in ran G$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
2	1	isf34lem2	$⊢ A \in {Fin}^{III} \to F : 𝒫 A ⟶ 𝒫 A$
3	2	adantr	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to F : 𝒫 A ⟶ 𝒫 A$
4	3	3adant3	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to F : 𝒫 A ⟶ 𝒫 A$
5	4	ffnd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to F Fn 𝒫 A$
6		imassrn	$⊢ F [ran G] \subseteq ran F$
7	3	frnd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ran F \subseteq 𝒫 A$
8	7	3adant3	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to ran F \subseteq 𝒫 A$
9	6 8	sstrid	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to F [ran G] \subseteq 𝒫 A$
10		simp1	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to A \in {Fin}^{III}$
11		fco	$⊢ (F : 𝒫 A ⟶ 𝒫 A \land G : ω ⟶ 𝒫 A) \to (F \circ G) : ω ⟶ 𝒫 A$
12	2 11	sylan	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to (F \circ G) : ω ⟶ 𝒫 A$
13	12	3adant3	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to (F \circ G) : ω ⟶ 𝒫 A$
14		sscon	$⊢ G (y) \subseteq G (suc y) \to A ∖ G (suc y) \subseteq A ∖ G (y)$
15		simpr	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to G : ω ⟶ 𝒫 A$
16		peano2	$⊢ y \in ω \to suc y \in ω$
17		fvco3	$⊢ (G : ω ⟶ 𝒫 A \land suc y \in ω) \to (F \circ G) (suc y) = F (G (suc y))$
18	15 16 17	syl2an	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to (F \circ G) (suc y) = F (G (suc y))$
19		simpll	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to A \in {Fin}^{III}$
20		ffvelrn	$⊢ (G : ω ⟶ 𝒫 A \land suc y \in ω) \to G (suc y) \in 𝒫 A$
21	15 16 20	syl2an	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to G (suc y) \in 𝒫 A$
22	21	elpwid	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to G (suc y) \subseteq A$
23	1	isf34lem1	$⊢ (A \in {Fin}^{III} \land G (suc y) \subseteq A) \to F (G (suc y)) = A ∖ G (suc y)$
24	19 22 23	syl2anc	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to F (G (suc y)) = A ∖ G (suc y)$
25	18 24	eqtrd	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to (F \circ G) (suc y) = A ∖ G (suc y)$
26		fvco3	$⊢ (G : ω ⟶ 𝒫 A \land y \in ω) \to (F \circ G) (y) = F (G (y))$
27	26	adantll	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to (F \circ G) (y) = F (G (y))$
28		ffvelrn	$⊢ (G : ω ⟶ 𝒫 A \land y \in ω) \to G (y) \in 𝒫 A$
29	28	adantll	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to G (y) \in 𝒫 A$
30	29	elpwid	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to G (y) \subseteq A$
31	1	isf34lem1	$⊢ (A \in {Fin}^{III} \land G (y) \subseteq A) \to F (G (y)) = A ∖ G (y)$
32	19 30 31	syl2anc	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to F (G (y)) = A ∖ G (y)$
33	27 32	eqtrd	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to (F \circ G) (y) = A ∖ G (y)$
34	25 33	sseq12d	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to ((F \circ G) (suc y) \subseteq (F \circ G) (y) \leftrightarrow A ∖ G (suc y) \subseteq A ∖ G (y))$
35	14 34	syl5ibr	$⊢ ((A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \land y \in ω) \to (G (y) \subseteq G (suc y) \to (F \circ G) (suc y) \subseteq (F \circ G) (y))$
36	35	ralimdva	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to (\forall y \in ω G (y) \subseteq G (suc y) \to \forall y \in ω (F \circ G) (suc y) \subseteq (F \circ G) (y))$
37	36	3impia	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to \forall y \in ω (F \circ G) (suc y) \subseteq (F \circ G) (y)$
38		fin33i	$⊢ (A \in {Fin}^{III} \land (F \circ G) : ω ⟶ 𝒫 A \land \forall y \in ω (F \circ G) (suc y) \subseteq (F \circ G) (y)) \to ⋂ ran (F \circ G) \in ran (F \circ G)$
39	10 13 37 38	syl3anc	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to ⋂ ran (F \circ G) \in ran (F \circ G)$
40		rnco2	$⊢ ran (F \circ G) = F [ran G]$
41	40	inteqi	$⊢ ⋂ ran (F \circ G) = ⋂ F [ran G]$
42	39 41 40	3eltr3g	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to ⋂ F [ran G] \in F [ran G]$
43		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]]$
44	5 9 42 43	syl3anc	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to F (⋂ F [ran G]) \in F [F [ran G]]$
45		simpl	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to A \in {Fin}^{III}$
46	6 7	sstrid	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to F [ran G] \subseteq 𝒫 A$
47		incom	$⊢ dom F \cap ran G = ran G \cap dom F$
48		frn	$⊢ G : ω ⟶ 𝒫 A \to ran G \subseteq 𝒫 A$
49	48	adantl	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ran G \subseteq 𝒫 A$
50	3	fdmd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to dom F = 𝒫 A$
51	49 50	sseqtrrd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ran G \subseteq dom F$
52		df-ss	$⊢ ran G \subseteq dom F \leftrightarrow ran G \cap dom F = ran G$
53	51 52	sylib	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ran G \cap dom F = ran G$
54	47 53	syl5eq	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to dom F \cap ran G = ran G$
55		fdm	$⊢ G : ω ⟶ 𝒫 A \to dom G = ω$
56	55	adantl	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to dom G = ω$
57		peano1	$⊢ \emptyset \in ω$
58		ne0i	$⊢ \emptyset \in ω \to ω \neq \emptyset$
59	57 58	mp1i	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ω \neq \emptyset$
60	56 59	eqnetrd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to dom G \neq \emptyset$
61		dm0rn0	$⊢ dom G = \emptyset \leftrightarrow ran G = \emptyset$
62	61	necon3bii	$⊢ dom G \neq \emptyset \leftrightarrow ran G \neq \emptyset$
63	60 62	sylib	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ran G \neq \emptyset$
64	54 63	eqnetrd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to dom F \cap ran G \neq \emptyset$
65		imadisj	$⊢ F [ran G] = \emptyset \leftrightarrow dom F \cap ran G = \emptyset$
66	65	necon3bii	$⊢ F [ran G] \neq \emptyset \leftrightarrow dom F \cap ran G \neq \emptyset$
67	64 66	sylibr	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to F [ran G] \neq \emptyset$
68	1	isf34lem5	$⊢ (A \in {Fin}^{III} \land (F [ran G] \subseteq 𝒫 A \land F [ran G] \neq \emptyset)) \to F (⋂ F [ran G]) = ⋃ F [F [ran G]]$
69	45 46 67 68	syl12anc	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to F (⋂ F [ran G]) = ⋃ F [F [ran G]]$
70	1	isf34lem3	$⊢ (A \in {Fin}^{III} \land ran G \subseteq 𝒫 A) \to F [F [ran G]] = ran G$
71	45 49 70	syl2anc	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to F [F [ran G]] = ran G$
72	71	unieqd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to ⋃ F [F [ran G]] = ⋃ ran G$
73	69 72	eqtrd	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to F (⋂ F [ran G]) = ⋃ ran G$
74	73 71	eleq12d	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A) \to (F (⋂ F [ran G]) \in F [F [ran G]] \leftrightarrow ⋃ ran G \in ran G)$
75	74	3adant3	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to (F (⋂ F [ran G]) \in F [F [ran G]] \leftrightarrow ⋃ ran G \in ran G)$
76	44 75	mpbid	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall y \in ω G (y) \subseteq G (suc y)) \to ⋃ ran G \in ran G$

Metamath Proof Explorer

Theorem isf34lem7

Proof