fin23lem32

Description: Lemma for fin23 . Wrap the previous construction into a function to hide the hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem.a	$⊢ U = {seq}_{ω} ((i \in ω, u \in V ⟼ if (t (i) \cap u = \emptyset, u, t (i) \cap u)), ⋃ ran t)$
	fin23lem17.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	fin23lem.b	$⊢ P = \{v \in ω \| ⋂ ran U \subseteq t (v)\}$
	fin23lem.c	$⊢ Q = (w \in ω ⟼ (ι x \in P \| (x \cap P) \approx w))$
	fin23lem.d	$⊢ R = (w \in ω ⟼ (ι x \in (ω ∖ P) \| (x \cap (ω ∖ P)) \approx w))$
	fin23lem.e	$⊢ Z = if (P \in Fin, t \circ R, (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
Assertion	fin23lem32	$⊢ G \in F \to \exists f \forall b ((b : ω \underset{1-1}{⟶} V \land ⋃ ran b \subseteq G) \to (f (b) : ω \underset{1-1}{⟶} V \land ⋃ ran f (b) \subset ⋃ ran b))$

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	$⊢ U = {seq}_{ω} ((i \in ω, u \in V ⟼ if (t (i) \cap u = \emptyset, u, t (i) \cap u)), ⋃ ran t)$
2		fin23lem17.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
3		fin23lem.b	$⊢ P = \{v \in ω \| ⋂ ran U \subseteq t (v)\}$
4		fin23lem.c	$⊢ Q = (w \in ω ⟼ (ι x \in P \| (x \cap P) \approx w))$
5		fin23lem.d	$⊢ R = (w \in ω ⟼ (ι x \in (ω ∖ P) \| (x \cap (ω ∖ P)) \approx w))$
6		fin23lem.e	$⊢ Z = if (P \in Fin, t \circ R, (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
7	1 2 3 4 5 6	fin23lem28	$⊢ t : ω \underset{1-1}{⟶} V \to Z : ω \underset{1-1}{⟶} V$
8	7	ad2antrl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to Z : ω \underset{1-1}{⟶} V$
9		simprl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to t : ω \underset{1-1}{⟶} V$
10		simpl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to G \in F$
11		simprr	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to ⋃ ran t \subseteq G$
12	1 2 3 4 5 6	fin23lem31	$⊢ (t : ω \underset{1-1}{⟶} V \land G \in F \land ⋃ ran t \subseteq G) \to ⋃ ran Z \subset ⋃ ran t$
13	9 10 11 12	syl3anc	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to ⋃ ran Z \subset ⋃ ran t$
14		f1fn	$⊢ t : ω \underset{1-1}{⟶} V \to t Fn ω$
15		dffn3	$⊢ t Fn ω \leftrightarrow t : ω ⟶ ran t$
16	14 15	sylib	$⊢ t : ω \underset{1-1}{⟶} V \to t : ω ⟶ ran t$
17	16	ad2antrl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to t : ω ⟶ ran t$
18		sspwuni	$⊢ ran t \subseteq 𝒫 G \leftrightarrow ⋃ ran t \subseteq G$
19	18	biimpri	$⊢ ⋃ ran t \subseteq G \to ran t \subseteq 𝒫 G$
20	19	ad2antll	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to ran t \subseteq 𝒫 G$
21	17 20	fssd	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to t : ω ⟶ 𝒫 G$
22		pwexg	$⊢ G \in F \to 𝒫 G \in V$
23	22	adantr	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to 𝒫 G \in V$
24		vex	$⊢ t \in V$
25		f1f	$⊢ t : ω \underset{1-1}{⟶} V \to t : ω ⟶ V$
26		dmfex	$⊢ (t \in V \land t : ω ⟶ V) \to ω \in V$
27	24 25 26	sylancr	$⊢ t : ω \underset{1-1}{⟶} V \to ω \in V$
28	27	ad2antrl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to ω \in V$
29	23 28	elmapd	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to (t \in ({𝒫 G}^{ω}) \leftrightarrow t : ω ⟶ 𝒫 G)$
30	21 29	mpbird	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to t \in ({𝒫 G}^{ω})$
31		f1f	$⊢ Z : ω \underset{1-1}{⟶} V \to Z : ω ⟶ V$
32	8 31	syl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to Z : ω ⟶ V$
33	32 28	fexd	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to Z \in V$
34		eqid	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) = (t \in ({𝒫 G}^{ω}) ⟼ Z)$
35	34	fvmpt2	$⊢ (t \in ({𝒫 G}^{ω}) \land Z \in V) \to (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z$
36	30 33 35	syl2anc	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z$
37		f1eq1	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \leftrightarrow Z : ω \underset{1-1}{⟶} V)$
38		rneq	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = ran Z$
39	38	unieqd	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = ⋃ ran Z$
40	39	psseq1d	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to (⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t \leftrightarrow ⋃ ran Z \subset ⋃ ran t)$
41	37 40	anbi12d	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to (((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t) \leftrightarrow (Z : ω \underset{1-1}{⟶} V \land ⋃ ran Z \subset ⋃ ran t))$
42	36 41	syl	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to (((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t) \leftrightarrow (Z : ω \underset{1-1}{⟶} V \land ⋃ ran Z \subset ⋃ ran t))$
43	8 13 42	mpbir2and	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t)$
44	43	ex	$⊢ G \in F \to ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t))$
45	44	alrimiv	$⊢ G \in F \to \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t))$
46		ovex	$⊢ {𝒫 G}^{ω} \in V$
47	46	mptex	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) \in V$
48		nfmpt1	$⊢ \underline{Ⅎ} t (t \in ({𝒫 G}^{ω}) ⟼ Z)$
49	48	nfeq2	$⊢ Ⅎ t f = (t \in ({𝒫 G}^{ω}) ⟼ Z)$
50		fveq1	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to f (t) = (t \in ({𝒫 G}^{ω}) ⟼ Z) (t)$
51		f1eq1	$⊢ f (t) = (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \to (f (t) : ω \underset{1-1}{⟶} V \leftrightarrow (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V)$
52	50 51	syl	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to (f (t) : ω \underset{1-1}{⟶} V \leftrightarrow (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V)$
53	50	rneqd	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to ran f (t) = ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t)$
54	53	unieqd	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to ⋃ ran f (t) = ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t)$
55	54	psseq1d	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to (⋃ ran f (t) \subset ⋃ ran t \leftrightarrow ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t)$
56	52 55	anbi12d	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to ((f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t) \leftrightarrow ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t))$
57	56	imbi2d	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to (((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t)) \leftrightarrow ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t)))$
58	49 57	albid	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to (\forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t)) \leftrightarrow \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t)))$
59	47 58	spcev	$⊢ \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \land ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t)) \to \exists f \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t))$
60	45 59	syl	$⊢ G \in F \to \exists f \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t))$
61		f1eq1	$⊢ b = t \to (b : ω \underset{1-1}{⟶} V \leftrightarrow t : ω \underset{1-1}{⟶} V)$
62		rneq	$⊢ b = t \to ran b = ran t$
63	62	unieqd	$⊢ b = t \to ⋃ ran b = ⋃ ran t$
64	63	sseq1d	$⊢ b = t \to (⋃ ran b \subseteq G \leftrightarrow ⋃ ran t \subseteq G)$
65	61 64	anbi12d	$⊢ b = t \to ((b : ω \underset{1-1}{⟶} V \land ⋃ ran b \subseteq G) \leftrightarrow (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G))$
66		fveq2	$⊢ b = t \to f (b) = f (t)$
67		f1eq1	$⊢ f (b) = f (t) \to (f (b) : ω \underset{1-1}{⟶} V \leftrightarrow f (t) : ω \underset{1-1}{⟶} V)$
68	66 67	syl	$⊢ b = t \to (f (b) : ω \underset{1-1}{⟶} V \leftrightarrow f (t) : ω \underset{1-1}{⟶} V)$
69	66	rneqd	$⊢ b = t \to ran f (b) = ran f (t)$
70	69	unieqd	$⊢ b = t \to ⋃ ran f (b) = ⋃ ran f (t)$
71	70 63	psseq12d	$⊢ b = t \to (⋃ ran f (b) \subset ⋃ ran b \leftrightarrow ⋃ ran f (t) \subset ⋃ ran t)$
72	68 71	anbi12d	$⊢ b = t \to ((f (b) : ω \underset{1-1}{⟶} V \land ⋃ ran f (b) \subset ⋃ ran b) \leftrightarrow (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t))$
73	65 72	imbi12d	$⊢ b = t \to (((b : ω \underset{1-1}{⟶} V \land ⋃ ran b \subseteq G) \to (f (b) : ω \underset{1-1}{⟶} V \land ⋃ ran f (b) \subset ⋃ ran b)) \leftrightarrow ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t)))$
74	73	cbvalvw	$⊢ \forall b ((b : ω \underset{1-1}{⟶} V \land ⋃ ran b \subseteq G) \to (f (b) : ω \underset{1-1}{⟶} V \land ⋃ ran f (b) \subset ⋃ ran b)) \leftrightarrow \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t))$
75	74	exbii	$⊢ \exists f \forall b ((b : ω \underset{1-1}{⟶} V \land ⋃ ran b \subseteq G) \to (f (b) : ω \underset{1-1}{⟶} V \land ⋃ ran f (b) \subset ⋃ ran b)) \leftrightarrow \exists f \forall t ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G) \to (f (t) : ω \underset{1-1}{⟶} V \land ⋃ ran f (t) \subset ⋃ ran t))$
76	60 75	sylibr	$⊢ G \in F \to \exists f \forall b ((b : ω \underset{1-1}{⟶} V \land ⋃ ran b \subseteq G) \to (f (b) : ω \underset{1-1}{⟶} V \land ⋃ ran f (b) \subset ⋃ ran b))$

Metamath Proof Explorer

Theorem fin23lem32

Proof