fin23lem39

Description: Lemma for fin23 . Thus, we have that g could not have been in F after all. (Contributed by Stefan O'Rear, 4-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem33.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	fin23lem.f	$⊢ φ \to h : ω \underset{1-1}{⟶} V$
	fin23lem.g	$⊢ φ \to ⋃ ran h \subseteq G$
	fin23lem.h	$⊢ φ \to \forall j ((j : ω \underset{1-1}{⟶} V \land ⋃ ran j \subseteq G) \to (i (j) : ω \underset{1-1}{⟶} V \land ⋃ ran i (j) \subset ⋃ ran j))$
	fin23lem.i	$⊢ Y = {rec (i, h) ↾}_{ω}$
Assertion	fin23lem39	$⊢ φ \to \neg G \in F$

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		fin23lem.f	$⊢ φ \to h : ω \underset{1-1}{⟶} V$
3		fin23lem.g	$⊢ φ \to ⋃ ran h \subseteq G$
4		fin23lem.h	$⊢ φ \to \forall j ((j : ω \underset{1-1}{⟶} V \land ⋃ ran j \subseteq G) \to (i (j) : ω \underset{1-1}{⟶} V \land ⋃ ran i (j) \subset ⋃ ran j))$
5		fin23lem.i	$⊢ Y = {rec (i, h) ↾}_{ω}$
6	1 2 3 4 5	fin23lem38	$⊢ φ \to \neg ⋂ ran (c \in ω ⟼ ⋃ ran Y (c)) \in ran (c \in ω ⟼ ⋃ ran Y (c))$
7	1 2 3 4 5	fin23lem35	$⊢ (φ \land e \in ω) \to ⋃ ran Y (suc e) \subset ⋃ ran Y (e)$
8	7	pssssd	$⊢ (φ \land e \in ω) \to ⋃ ran Y (suc e) \subseteq ⋃ ran Y (e)$
9		peano2	$⊢ e \in ω \to suc e \in ω$
10		fveq2	$⊢ c = suc e \to Y (c) = Y (suc e)$
11	10	rneqd	$⊢ c = suc e \to ran Y (c) = ran Y (suc e)$
12	11	unieqd	$⊢ c = suc e \to ⋃ ran Y (c) = ⋃ ran Y (suc e)$
13		eqid	$⊢ (c \in ω ⟼ ⋃ ran Y (c)) = (c \in ω ⟼ ⋃ ran Y (c))$
14		fvex	$⊢ Y (suc e) \in V$
15	14	rnex	$⊢ ran Y (suc e) \in V$
16	15	uniex	$⊢ ⋃ ran Y (suc e) \in V$
17	12 13 16	fvmpt	$⊢ suc e \in ω \to (c \in ω ⟼ ⋃ ran Y (c)) (suc e) = ⋃ ran Y (suc e)$
18	9 17	syl	$⊢ e \in ω \to (c \in ω ⟼ ⋃ ran Y (c)) (suc e) = ⋃ ran Y (suc e)$
19		fveq2	$⊢ c = e \to Y (c) = Y (e)$
20	19	rneqd	$⊢ c = e \to ran Y (c) = ran Y (e)$
21	20	unieqd	$⊢ c = e \to ⋃ ran Y (c) = ⋃ ran Y (e)$
22		fvex	$⊢ Y (e) \in V$
23	22	rnex	$⊢ ran Y (e) \in V$
24	23	uniex	$⊢ ⋃ ran Y (e) \in V$
25	21 13 24	fvmpt	$⊢ e \in ω \to (c \in ω ⟼ ⋃ ran Y (c)) (e) = ⋃ ran Y (e)$
26	18 25	sseq12d	$⊢ e \in ω \to ((c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e) \leftrightarrow ⋃ ran Y (suc e) \subseteq ⋃ ran Y (e))$
27	26	adantl	$⊢ (φ \land e \in ω) \to ((c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e) \leftrightarrow ⋃ ran Y (suc e) \subseteq ⋃ ran Y (e))$
28	8 27	mpbird	$⊢ (φ \land e \in ω) \to (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e)$
29	28	ralrimiva	$⊢ φ \to \forall e \in ω (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e)$
30	29	adantr	$⊢ (φ \land G \in F) \to \forall e \in ω (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e)$
31		fveq1	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to d (suc e) = (c \in ω ⟼ ⋃ ran Y (c)) (suc e)$
32		fveq1	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to d (e) = (c \in ω ⟼ ⋃ ran Y (c)) (e)$
33	31 32	sseq12d	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to (d (suc e) \subseteq d (e) \leftrightarrow (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e))$
34	33	ralbidv	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to (\forall e \in ω d (suc e) \subseteq d (e) \leftrightarrow \forall e \in ω (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e))$
35		rneq	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to ran d = ran (c \in ω ⟼ ⋃ ran Y (c))$
36	35	inteqd	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to ⋂ ran d = ⋂ ran (c \in ω ⟼ ⋃ ran Y (c))$
37	36 35	eleq12d	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to (⋂ ran d \in ran d \leftrightarrow ⋂ ran (c \in ω ⟼ ⋃ ran Y (c)) \in ran (c \in ω ⟼ ⋃ ran Y (c)))$
38	34 37	imbi12d	$⊢ d = (c \in ω ⟼ ⋃ ran Y (c)) \to ((\forall e \in ω d (suc e) \subseteq d (e) \to ⋂ ran d \in ran d) \leftrightarrow (\forall e \in ω (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e) \to ⋂ ran (c \in ω ⟼ ⋃ ran Y (c)) \in ran (c \in ω ⟼ ⋃ ran Y (c))))$
39	1	isfin3ds	$⊢ G \in F \to (G \in F \leftrightarrow \forall d \in ({𝒫 G}^{ω}) (\forall e \in ω d (suc e) \subseteq d (e) \to ⋂ ran d \in ran d))$
40	39	ibi	$⊢ G \in F \to \forall d \in ({𝒫 G}^{ω}) (\forall e \in ω d (suc e) \subseteq d (e) \to ⋂ ran d \in ran d)$
41	40	adantl	$⊢ (φ \land G \in F) \to \forall d \in ({𝒫 G}^{ω}) (\forall e \in ω d (suc e) \subseteq d (e) \to ⋂ ran d \in ran d)$
42	1 2 3 4 5	fin23lem34	$⊢ (φ \land c \in ω) \to (Y (c) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (c) \subseteq G)$
43	42	simprd	$⊢ (φ \land c \in ω) \to ⋃ ran Y (c) \subseteq G$
44	43	adantlr	$⊢ ((φ \land G \in F) \land c \in ω) \to ⋃ ran Y (c) \subseteq G$
45		elpw2g	$⊢ G \in F \to (⋃ ran Y (c) \in 𝒫 G \leftrightarrow ⋃ ran Y (c) \subseteq G)$
46	45	ad2antlr	$⊢ ((φ \land G \in F) \land c \in ω) \to (⋃ ran Y (c) \in 𝒫 G \leftrightarrow ⋃ ran Y (c) \subseteq G)$
47	44 46	mpbird	$⊢ ((φ \land G \in F) \land c \in ω) \to ⋃ ran Y (c) \in 𝒫 G$
48	47	fmpttd	$⊢ (φ \land G \in F) \to (c \in ω ⟼ ⋃ ran Y (c)) : ω ⟶ 𝒫 G$
49		pwexg	$⊢ G \in F \to 𝒫 G \in V$
50		vex	$⊢ h \in V$
51		f1f	$⊢ h : ω \underset{1-1}{⟶} V \to h : ω ⟶ V$
52		dmfex	$⊢ (h \in V \land h : ω ⟶ V) \to ω \in V$
53	50 51 52	sylancr	$⊢ h : ω \underset{1-1}{⟶} V \to ω \in V$
54	2 53	syl	$⊢ φ \to ω \in V$
55		elmapg	$⊢ (𝒫 G \in V \land ω \in V) \to ((c \in ω ⟼ ⋃ ran Y (c)) \in ({𝒫 G}^{ω}) \leftrightarrow (c \in ω ⟼ ⋃ ran Y (c)) : ω ⟶ 𝒫 G)$
56	49 54 55	syl2anr	$⊢ (φ \land G \in F) \to ((c \in ω ⟼ ⋃ ran Y (c)) \in ({𝒫 G}^{ω}) \leftrightarrow (c \in ω ⟼ ⋃ ran Y (c)) : ω ⟶ 𝒫 G)$
57	48 56	mpbird	$⊢ (φ \land G \in F) \to (c \in ω ⟼ ⋃ ran Y (c)) \in ({𝒫 G}^{ω})$
58	38 41 57	rspcdva	$⊢ (φ \land G \in F) \to (\forall e \in ω (c \in ω ⟼ ⋃ ran Y (c)) (suc e) \subseteq (c \in ω ⟼ ⋃ ran Y (c)) (e) \to ⋂ ran (c \in ω ⟼ ⋃ ran Y (c)) \in ran (c \in ω ⟼ ⋃ ran Y (c)))$
59	30 58	mpd	$⊢ (φ \land G \in F) \to ⋂ ran (c \in ω ⟼ ⋃ ran Y (c)) \in ran (c \in ω ⟼ ⋃ ran Y (c))$
60	6 59	mtand	$⊢ φ \to \neg G \in F$

Metamath Proof Explorer

Theorem fin23lem39

Proof