fin23lem33

Description: Lemma for fin23 . Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014)

		Ref	Expression
	Hypothesis	fin23lem33.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	Assertion	fin23lem33	$⊢ 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		fin23lem33.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
2		fveq2	$⊢ j = c \to e (j) = e (c)$
3	2	ineq1d	$⊢ j = c \to e (j) \cap k = e (c) \cap k$
4	3	eqeq1d	$⊢ j = c \to (e (j) \cap k = \emptyset \leftrightarrow e (c) \cap k = \emptyset)$
5	4 3	ifbieq2d	$⊢ j = c \to if (e (j) \cap k = \emptyset, k, e (j) \cap k) = if (e (c) \cap k = \emptyset, k, e (c) \cap k)$
6		ineq2	$⊢ k = d \to e (c) \cap k = e (c) \cap d$
7	6	eqeq1d	$⊢ k = d \to (e (c) \cap k = \emptyset \leftrightarrow e (c) \cap d = \emptyset)$
8		id	$⊢ k = d \to k = d$
9	7 8 6	ifbieq12d	$⊢ k = d \to if (e (c) \cap k = \emptyset, k, e (c) \cap k) = if (e (c) \cap d = \emptyset, d, e (c) \cap d)$
10	5 9	cbvmpov	$⊢ (j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)) = (c \in ω, d \in V ⟼ if (e (c) \cap d = \emptyset, d, e (c) \cap d))$
11		eqid	$⊢ ⋃ ran e = ⋃ ran e$
12		seqomeq12	$⊢ ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)) = (c \in ω, d \in V ⟼ if (e (c) \cap d = \emptyset, d, e (c) \cap d)) \land ⋃ ran e = ⋃ ran e) \to {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) = {seq}_{ω} ((c \in ω, d \in V ⟼ if (e (c) \cap d = \emptyset, d, e (c) \cap d)), ⋃ ran e)$
13	10 11 12	mp2an	$⊢ {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) = {seq}_{ω} ((c \in ω, d \in V ⟼ if (e (c) \cap d = \emptyset, d, e (c) \cap d)), ⋃ ran e)$
14		fveq2	$⊢ l = y \to e (l) = e (y)$
15	14	sseq2d	$⊢ l = y \to (⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l) \leftrightarrow ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (y))$
16	15	cbvrabv	$⊢ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} = \{y \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (y)\}$
17		eqid	$⊢ (g \in ω ⟼ (ι x \in \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} \| (x \cap \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \approx g)) = (g \in ω ⟼ (ι x \in \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} \| (x \cap \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \approx g))$
18		eqid	$⊢ (g \in ω ⟼ (ι x \in (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \| (x \cap (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\})) \approx g)) = (g \in ω ⟼ (ι x \in (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \| (x \cap (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\})) \approx g))$
19		eqid	$⊢ if (\{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} \in Fin, e \circ (g \in ω ⟼ (ι x \in (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \| (x \cap (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\})) \approx g)), (i \in \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} ⟼ e (i) ∖ ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e)) \circ (g \in ω ⟼ (ι x \in \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} \| (x \cap \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \approx g))) = if (\{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} \in Fin, e \circ (g \in ω ⟼ (ι x \in (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \| (x \cap (ω ∖ \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\})) \approx g)), (i \in \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} ⟼ e (i) ∖ ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e)) \circ (g \in ω ⟼ (ι x \in \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\} \| (x \cap \{l \in ω \| ⋂ ran {seq}_{ω} ((j \in ω, k \in V ⟼ if (e (j) \cap k = \emptyset, k, e (j) \cap k)), ⋃ ran e) \subseteq e (l)\}) \approx g)))$
20	13 1 16 17 18 19	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))$

Metamath Proof Explorer

Theorem fin23lem33

Proof