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		fex	$⊢ (Z : ω ⟶ V \land ω \in V) \to Z \in V$
34	32 28 33	syl2anc	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to Z \in V$
35		eqid	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) = (t \in ({𝒫 G}^{ω}) ⟼ Z)$
36	35	fvmpt2	$⊢ (t \in ({𝒫 G}^{ω}) \land Z \in V) \to (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z$
37	30 34 36	syl2anc	$⊢ (G \in F \land (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \subseteq G)) \to (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z$
38		f1eq1	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to ((t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V \leftrightarrow Z : ω \underset{1-1}{⟶} V)$
39		rneq	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = ran Z$
40	39	unieqd	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = ⋃ ran Z$
41	40	psseq1d	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) = Z \to (⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t \leftrightarrow ⋃ ran Z \subset ⋃ ran t)$
42	38 41	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))$
43	37 42	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))$
44	8 13 43	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)$
45	44	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))$
46	45	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))$
47		ovex	$⊢ {𝒫 G}^{ω} \in V$
48	47	mptex	$⊢ (t \in ({𝒫 G}^{ω}) ⟼ Z) \in V$
49		nfmpt1	$⊢ \underline{Ⅎ} t (t \in ({𝒫 G}^{ω}) ⟼ Z)$
50	49	nfeq2	$⊢ Ⅎ t f = (t \in ({𝒫 G}^{ω}) ⟼ Z)$
51		fveq1	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to f (t) = (t \in ({𝒫 G}^{ω}) ⟼ Z) (t)$
52		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)$
53	51 52	syl	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to (f (t) : ω \underset{1-1}{⟶} V \leftrightarrow (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) : ω \underset{1-1}{⟶} V)$
54	51	rneqd	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to ran f (t) = ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t)$
55	54	unieqd	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to ⋃ ran f (t) = ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t)$
56	55	psseq1d	$⊢ f = (t \in ({𝒫 G}^{ω}) ⟼ Z) \to (⋃ ran f (t) \subset ⋃ ran t \leftrightarrow ⋃ ran (t \in ({𝒫 G}^{ω}) ⟼ Z) (t) \subset ⋃ ran t)$
57	53 56	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))$
58	57	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)))$
59	50 58	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)))$
60	48 59	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))$
61	46 60	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))$
62		f1eq1	$⊢ b = t \to (b : ω \underset{1-1}{⟶} V \leftrightarrow t : ω \underset{1-1}{⟶} V)$
63		rneq	$⊢ b = t \to ran b = ran t$
64	63	unieqd	$⊢ b = t \to ⋃ ran b = ⋃ ran t$
65	64	sseq1d	$⊢ b = t \to (⋃ ran b \subseteq G \leftrightarrow ⋃ ran t \subseteq G)$
66	62 65	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))$
67		fveq2	$⊢ b = t \to f (b) = f (t)$
68		f1eq1	$⊢ f (b) = f (t) \to (f (b) : ω \underset{1-1}{⟶} V \leftrightarrow f (t) : ω \underset{1-1}{⟶} V)$
69	67 68	syl	$⊢ b = t \to (f (b) : ω \underset{1-1}{⟶} V \leftrightarrow f (t) : ω \underset{1-1}{⟶} V)$
70	67	rneqd	$⊢ b = t \to ran f (b) = ran f (t)$
71	70	unieqd	$⊢ b = t \to ⋃ ran f (b) = ⋃ ran f (t)$
72	71 64	psseq12d	$⊢ b = t \to (⋃ ran f (b) \subset ⋃ ran b \leftrightarrow ⋃ ran f (t) \subset ⋃ ran t)$
73	69 72	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))$
74	66 73	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)))$
75	74	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))$
76	75	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))$
77	61 76	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