fin23lem38

Description: Lemma for fin23 . The contradictory chain has no minimum. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

	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	fin23lem38	$⊢ φ \to \neg ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \in ran (b \in ω ⟼ ⋃ ran Y (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		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		peano2	$⊢ d \in ω \to suc d \in ω$
7		eqid	$⊢ ⋃ ran Y (suc d) = ⋃ ran Y (suc d)$
8		fveq2	$⊢ b = suc d \to Y (b) = Y (suc d)$
9	8	rneqd	$⊢ b = suc d \to ran Y (b) = ran Y (suc d)$
10	9	unieqd	$⊢ b = suc d \to ⋃ ran Y (b) = ⋃ ran Y (suc d)$
11	10	rspceeqv	$⊢ (suc d \in ω \land ⋃ ran Y (suc d) = ⋃ ran Y (suc d)) \to \exists b \in ω ⋃ ran Y (suc d) = ⋃ ran Y (b)$
12	7 11	mpan2	$⊢ suc d \in ω \to \exists b \in ω ⋃ ran Y (suc d) = ⋃ ran Y (b)$
13		fvex	$⊢ Y (suc d) \in V$
14	13	rnex	$⊢ ran Y (suc d) \in V$
15	14	uniex	$⊢ ⋃ ran Y (suc d) \in V$
16		eqid	$⊢ (b \in ω ⟼ ⋃ ran Y (b)) = (b \in ω ⟼ ⋃ ran Y (b))$
17	16	elrnmpt	$⊢ ⋃ ran Y (suc d) \in V \to (⋃ ran Y (suc d) \in ran (b \in ω ⟼ ⋃ ran Y (b)) \leftrightarrow \exists b \in ω ⋃ ran Y (suc d) = ⋃ ran Y (b))$
18	15 17	ax-mp	$⊢ ⋃ ran Y (suc d) \in ran (b \in ω ⟼ ⋃ ran Y (b)) \leftrightarrow \exists b \in ω ⋃ ran Y (suc d) = ⋃ ran Y (b)$
19	12 18	sylibr	$⊢ suc d \in ω \to ⋃ ran Y (suc d) \in ran (b \in ω ⟼ ⋃ ran Y (b))$
20	6 19	syl	$⊢ d \in ω \to ⋃ ran Y (suc d) \in ran (b \in ω ⟼ ⋃ ran Y (b))$
21	20	adantl	$⊢ (φ \land d \in ω) \to ⋃ ran Y (suc d) \in ran (b \in ω ⟼ ⋃ ran Y (b))$
22		intss1	$⊢ ⋃ ran Y (suc d) \in ran (b \in ω ⟼ ⋃ ran Y (b)) \to ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \subseteq ⋃ ran Y (suc d)$
23	21 22	syl	$⊢ (φ \land d \in ω) \to ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \subseteq ⋃ ran Y (suc d)$
24	1 2 3 4 5	fin23lem35	$⊢ (φ \land d \in ω) \to ⋃ ran Y (suc d) \subset ⋃ ran Y (d)$
25	23 24	sspsstrd	$⊢ (φ \land d \in ω) \to ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \subset ⋃ ran Y (d)$
26		dfpss2	$⊢ ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \subset ⋃ ran Y (d) \leftrightarrow (⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \subseteq ⋃ ran Y (d) \land \neg ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) = ⋃ ran Y (d))$
27	26	simprbi	$⊢ ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \subset ⋃ ran Y (d) \to \neg ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) = ⋃ ran Y (d)$
28	25 27	syl	$⊢ (φ \land d \in ω) \to \neg ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) = ⋃ ran Y (d)$
29	28	nrexdv	$⊢ φ \to \neg \exists d \in ω ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) = ⋃ ran Y (d)$
30		fveq2	$⊢ b = d \to Y (b) = Y (d)$
31	30	rneqd	$⊢ b = d \to ran Y (b) = ran Y (d)$
32	31	unieqd	$⊢ b = d \to ⋃ ran Y (b) = ⋃ ran Y (d)$
33	32	cbvmptv	$⊢ (b \in ω ⟼ ⋃ ran Y (b)) = (d \in ω ⟼ ⋃ ran Y (d))$
34	33	elrnmpt	$⊢ ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \in ran (b \in ω ⟼ ⋃ ran Y (b)) \to (⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \in ran (b \in ω ⟼ ⋃ ran Y (b)) \leftrightarrow \exists d \in ω ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) = ⋃ ran Y (d))$
35	34	ibi	$⊢ ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \in ran (b \in ω ⟼ ⋃ ran Y (b)) \to \exists d \in ω ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) = ⋃ ran Y (d)$
36	29 35	nsyl	$⊢ φ \to \neg ⋂ ran (b \in ω ⟼ ⋃ ran Y (b)) \in ran (b \in ω ⟼ ⋃ ran Y (b))$

Metamath Proof Explorer

Theorem fin23lem38

Proof