fin23lem34

Description: Lemma for fin23 . Establish induction invariants on Y which parameterizes our contradictory chain of subsets. In this section, h is the hypothetically assumed family of subsets, g is the ground set, and i is the induction function constructed in the previous section. (Contributed by Stefan O'Rear, 2-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	fin23lem34	$⊢ (φ \land A \in ω) \to (Y (A) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (A) \subseteq G)$

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		fveq2	$⊢ a = \emptyset \to Y (a) = Y (\emptyset)$
7		f1eq1	$⊢ Y (a) = Y (\emptyset) \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (\emptyset) : ω \underset{1-1}{⟶} V)$
8	6 7	syl	$⊢ a = \emptyset \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (\emptyset) : ω \underset{1-1}{⟶} V)$
9	6	rneqd	$⊢ a = \emptyset \to ran Y (a) = ran Y (\emptyset)$
10	9	unieqd	$⊢ a = \emptyset \to ⋃ ran Y (a) = ⋃ ran Y (\emptyset)$
11	10	sseq1d	$⊢ a = \emptyset \to (⋃ ran Y (a) \subseteq G \leftrightarrow ⋃ ran Y (\emptyset) \subseteq G)$
12	8 11	anbi12d	$⊢ a = \emptyset \to ((Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G) \leftrightarrow (Y (\emptyset) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (\emptyset) \subseteq G))$
13	12	imbi2d	$⊢ a = \emptyset \to ((φ \to (Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G)) \leftrightarrow (φ \to (Y (\emptyset) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (\emptyset) \subseteq G)))$
14		fveq2	$⊢ a = b \to Y (a) = Y (b)$
15		f1eq1	$⊢ Y (a) = Y (b) \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (b) : ω \underset{1-1}{⟶} V)$
16	14 15	syl	$⊢ a = b \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (b) : ω \underset{1-1}{⟶} V)$
17	14	rneqd	$⊢ a = b \to ran Y (a) = ran Y (b)$
18	17	unieqd	$⊢ a = b \to ⋃ ran Y (a) = ⋃ ran Y (b)$
19	18	sseq1d	$⊢ a = b \to (⋃ ran Y (a) \subseteq G \leftrightarrow ⋃ ran Y (b) \subseteq G)$
20	16 19	anbi12d	$⊢ a = b \to ((Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G) \leftrightarrow (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G))$
21	20	imbi2d	$⊢ a = b \to ((φ \to (Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G)) \leftrightarrow (φ \to (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)))$
22		fveq2	$⊢ a = suc b \to Y (a) = Y (suc b)$
23		f1eq1	$⊢ Y (a) = Y (suc b) \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (suc b) : ω \underset{1-1}{⟶} V)$
24	22 23	syl	$⊢ a = suc b \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (suc b) : ω \underset{1-1}{⟶} V)$
25	22	rneqd	$⊢ a = suc b \to ran Y (a) = ran Y (suc b)$
26	25	unieqd	$⊢ a = suc b \to ⋃ ran Y (a) = ⋃ ran Y (suc b)$
27	26	sseq1d	$⊢ a = suc b \to (⋃ ran Y (a) \subseteq G \leftrightarrow ⋃ ran Y (suc b) \subseteq G)$
28	24 27	anbi12d	$⊢ a = suc b \to ((Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G) \leftrightarrow (Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G))$
29	28	imbi2d	$⊢ a = suc b \to ((φ \to (Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G)) \leftrightarrow (φ \to (Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G)))$
30		fveq2	$⊢ a = A \to Y (a) = Y (A)$
31		f1eq1	$⊢ Y (a) = Y (A) \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (A) : ω \underset{1-1}{⟶} V)$
32	30 31	syl	$⊢ a = A \to (Y (a) : ω \underset{1-1}{⟶} V \leftrightarrow Y (A) : ω \underset{1-1}{⟶} V)$
33	30	rneqd	$⊢ a = A \to ran Y (a) = ran Y (A)$
34	33	unieqd	$⊢ a = A \to ⋃ ran Y (a) = ⋃ ran Y (A)$
35	34	sseq1d	$⊢ a = A \to (⋃ ran Y (a) \subseteq G \leftrightarrow ⋃ ran Y (A) \subseteq G)$
36	32 35	anbi12d	$⊢ a = A \to ((Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G) \leftrightarrow (Y (A) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (A) \subseteq G))$
37	36	imbi2d	$⊢ a = A \to ((φ \to (Y (a) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (a) \subseteq G)) \leftrightarrow (φ \to (Y (A) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (A) \subseteq G)))$
38	5	fveq1i	$⊢ Y (\emptyset) = ({rec (i, h) ↾}_{ω}) (\emptyset)$
39		fr0g	$⊢ h \in V \to ({rec (i, h) ↾}_{ω}) (\emptyset) = h$
40	39	elv	$⊢ ({rec (i, h) ↾}_{ω}) (\emptyset) = h$
41	38 40	eqtri	$⊢ Y (\emptyset) = h$
42		f1eq1	$⊢ Y (\emptyset) = h \to (Y (\emptyset) : ω \underset{1-1}{⟶} V \leftrightarrow h : ω \underset{1-1}{⟶} V)$
43	41 42	ax-mp	$⊢ Y (\emptyset) : ω \underset{1-1}{⟶} V \leftrightarrow h : ω \underset{1-1}{⟶} V$
44	41	rneqi	$⊢ ran Y (\emptyset) = ran h$
45	44	unieqi	$⊢ ⋃ ran Y (\emptyset) = ⋃ ran h$
46	45	sseq1i	$⊢ ⋃ ran Y (\emptyset) \subseteq G \leftrightarrow ⋃ ran h \subseteq G$
47	43 46	anbi12i	$⊢ (Y (\emptyset) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (\emptyset) \subseteq G) \leftrightarrow (h : ω \underset{1-1}{⟶} V \land ⋃ ran h \subseteq G)$
48	2 3 47	sylanbrc	$⊢ φ \to (Y (\emptyset) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (\emptyset) \subseteq G)$
49		fvex	$⊢ Y (b) \in V$
50		f1eq1	$⊢ j = Y (b) \to (j : ω \underset{1-1}{⟶} V \leftrightarrow Y (b) : ω \underset{1-1}{⟶} V)$
51		rneq	$⊢ j = Y (b) \to ran j = ran Y (b)$
52	51	unieqd	$⊢ j = Y (b) \to ⋃ ran j = ⋃ ran Y (b)$
53	52	sseq1d	$⊢ j = Y (b) \to (⋃ ran j \subseteq G \leftrightarrow ⋃ ran Y (b) \subseteq G)$
54	50 53	anbi12d	$⊢ j = Y (b) \to ((j : ω \underset{1-1}{⟶} V \land ⋃ ran j \subseteq G) \leftrightarrow (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G))$
55		fveq2	$⊢ j = Y (b) \to i (j) = i (Y (b))$
56		f1eq1	$⊢ i (j) = i (Y (b)) \to (i (j) : ω \underset{1-1}{⟶} V \leftrightarrow i (Y (b)) : ω \underset{1-1}{⟶} V)$
57	55 56	syl	$⊢ j = Y (b) \to (i (j) : ω \underset{1-1}{⟶} V \leftrightarrow i (Y (b)) : ω \underset{1-1}{⟶} V)$
58	55	rneqd	$⊢ j = Y (b) \to ran i (j) = ran i (Y (b))$
59	58	unieqd	$⊢ j = Y (b) \to ⋃ ran i (j) = ⋃ ran i (Y (b))$
60	59 52	psseq12d	$⊢ j = Y (b) \to (⋃ ran i (j) \subset ⋃ ran j \leftrightarrow ⋃ ran i (Y (b)) \subset ⋃ ran Y (b))$
61	57 60	anbi12d	$⊢ j = Y (b) \to ((i (j) : ω \underset{1-1}{⟶} V \land ⋃ ran i (j) \subset ⋃ ran j) \leftrightarrow (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b)))$
62	54 61	imbi12d	$⊢ j = Y (b) \to (((j : ω \underset{1-1}{⟶} V \land ⋃ ran j \subseteq G) \to (i (j) : ω \underset{1-1}{⟶} V \land ⋃ ran i (j) \subset ⋃ ran j)) \leftrightarrow ((Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b))))$
63	49 62	spcv	$⊢ \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)) \to ((Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b)))$
64	4 63	syl	$⊢ φ \to ((Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b)))$
65	64	imp	$⊢ (φ \land (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b))$
66		pssss	$⊢ ⋃ ran i (Y (b)) \subset ⋃ ran Y (b) \to ⋃ ran i (Y (b)) \subseteq ⋃ ran Y (b)$
67		sstr	$⊢ (⋃ ran i (Y (b)) \subseteq ⋃ ran Y (b) \land ⋃ ran Y (b) \subseteq G) \to ⋃ ran i (Y (b)) \subseteq G$
68	66 67	sylan	$⊢ (⋃ ran i (Y (b)) \subset ⋃ ran Y (b) \land ⋃ ran Y (b) \subseteq G) \to ⋃ ran i (Y (b)) \subseteq G$
69	68	expcom	$⊢ ⋃ ran Y (b) \subseteq G \to (⋃ ran i (Y (b)) \subset ⋃ ran Y (b) \to ⋃ ran i (Y (b)) \subseteq G)$
70	69	anim2d	$⊢ ⋃ ran Y (b) \subseteq G \to ((i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b)) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G))$
71	70	ad2antll	$⊢ (φ \land (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to ((i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subset ⋃ ran Y (b)) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G))$
72	65 71	mpd	$⊢ (φ \land (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G)$
73	72	3adant1	$⊢ (b \in ω \land φ \land (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G)$
74		frsuc	$⊢ b \in ω \to ({rec (i, h) ↾}_{ω}) (suc b) = i (({rec (i, h) ↾}_{ω}) (b))$
75	5	fveq1i	$⊢ Y (suc b) = ({rec (i, h) ↾}_{ω}) (suc b)$
76	5	fveq1i	$⊢ Y (b) = ({rec (i, h) ↾}_{ω}) (b)$
77	76	fveq2i	$⊢ i (Y (b)) = i (({rec (i, h) ↾}_{ω}) (b))$
78	74 75 77	3eqtr4g	$⊢ b \in ω \to Y (suc b) = i (Y (b))$
79		f1eq1	$⊢ Y (suc b) = i (Y (b)) \to (Y (suc b) : ω \underset{1-1}{⟶} V \leftrightarrow i (Y (b)) : ω \underset{1-1}{⟶} V)$
80		rneq	$⊢ Y (suc b) = i (Y (b)) \to ran Y (suc b) = ran i (Y (b))$
81	80	unieqd	$⊢ Y (suc b) = i (Y (b)) \to ⋃ ran Y (suc b) = ⋃ ran i (Y (b))$
82	81	sseq1d	$⊢ Y (suc b) = i (Y (b)) \to (⋃ ran Y (suc b) \subseteq G \leftrightarrow ⋃ ran i (Y (b)) \subseteq G)$
83	79 82	anbi12d	$⊢ Y (suc b) = i (Y (b)) \to ((Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G) \leftrightarrow (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G))$
84	78 83	syl	$⊢ b \in ω \to ((Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G) \leftrightarrow (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G))$
85	84	3ad2ant1	$⊢ (b \in ω \land φ \land (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to ((Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G) \leftrightarrow (i (Y (b)) : ω \underset{1-1}{⟶} V \land ⋃ ran i (Y (b)) \subseteq G))$
86	73 85	mpbird	$⊢ (b \in ω \land φ \land (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to (Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G)$
87	86	3exp	$⊢ b \in ω \to (φ \to ((Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G) \to (Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G)))$
88	87	a2d	$⊢ b \in ω \to ((φ \to (Y (b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (b) \subseteq G)) \to (φ \to (Y (suc b) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (suc b) \subseteq G)))$
89	13 21 29 37 48 88	finds	$⊢ A \in ω \to (φ \to (Y (A) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (A) \subseteq G))$
90	89	impcom	$⊢ (φ \land A \in ω) \to (Y (A) : ω \underset{1-1}{⟶} V \land ⋃ ran Y (A) \subseteq G)$

Metamath Proof Explorer

Theorem fin23lem34

Proof