isf32lem2

Description: Lemma for isfin3-2 . Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014)

	Ref	Expression
Hypotheses	isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
	isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
	isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
Assertion	isf32lem2	$⊢ (φ \land A \in ω) \to \exists a \in ω (A \in a \land F (suc a) \subset F (a))$

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
2		isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
3		isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
4	3	adantr	$⊢ (φ \land A \in ω) \to \neg ⋂ ran F \in ran F$
5	1	ffnd	$⊢ φ \to F Fn ω$
6		peano2	$⊢ A \in ω \to suc A \in ω$
7		fnfvelrn	$⊢ (F Fn ω \land suc A \in ω) \to F (suc A) \in ran F$
8	5 6 7	syl2an	$⊢ (φ \land A \in ω) \to F (suc A) \in ran F$
9	8	adantr	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to F (suc A) \in ran F$
10		intss1	$⊢ F (suc A) \in ran F \to ⋂ ran F \subseteq F (suc A)$
11	9 10	syl	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to ⋂ ran F \subseteq F (suc A)$
12		fvelrnb	$⊢ F Fn ω \to (b \in ran F \leftrightarrow \exists c \in ω F (c) = b)$
13	5 12	syl	$⊢ φ \to (b \in ran F \leftrightarrow \exists c \in ω F (c) = b)$
14	13	ad2antrr	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to (b \in ran F \leftrightarrow \exists c \in ω F (c) = b)$
15		simplrr	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land suc A \subseteq c) \to c \in ω$
16	6	ad3antlr	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land suc A \subseteq c) \to suc A \in ω$
17		simpr	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land suc A \subseteq c) \to suc A \subseteq c$
18		simplrl	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land suc A \subseteq c) \to \forall a \in ω (A \in a \to F (suc a) = F (a))$
19		fveq2	$⊢ b = suc A \to F (b) = F (suc A)$
20	19	eqeq2d	$⊢ b = suc A \to (F (suc A) = F (b) \leftrightarrow F (suc A) = F (suc A))$
21	20	imbi2d	$⊢ b = suc A \to ((\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (b)) \leftrightarrow (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (suc A)))$
22		fveq2	$⊢ b = d \to F (b) = F (d)$
23	22	eqeq2d	$⊢ b = d \to (F (suc A) = F (b) \leftrightarrow F (suc A) = F (d))$
24	23	imbi2d	$⊢ b = d \to ((\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (b)) \leftrightarrow (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (d)))$
25		fveq2	$⊢ b = suc d \to F (b) = F (suc d)$
26	25	eqeq2d	$⊢ b = suc d \to (F (suc A) = F (b) \leftrightarrow F (suc A) = F (suc d))$
27	26	imbi2d	$⊢ b = suc d \to ((\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (b)) \leftrightarrow (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (suc d)))$
28		fveq2	$⊢ b = c \to F (b) = F (c)$
29	28	eqeq2d	$⊢ b = c \to (F (suc A) = F (b) \leftrightarrow F (suc A) = F (c))$
30	29	imbi2d	$⊢ b = c \to ((\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (b)) \leftrightarrow (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (c)))$
31		eqid	$⊢ F (suc A) = F (suc A)$
32	31	2a1i	$⊢ suc A \in ω \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (suc A))$
33		elex	$⊢ suc A \in ω \to suc A \in V$
34		sucexb	$⊢ A \in V \leftrightarrow suc A \in V$
35	33 34	sylibr	$⊢ suc A \in ω \to A \in V$
36	35	adantl	$⊢ (d \in ω \land suc A \in ω) \to A \in V$
37		sucssel	$⊢ A \in V \to (suc A \subseteq d \to A \in d)$
38	36 37	syl	$⊢ (d \in ω \land suc A \in ω) \to (suc A \subseteq d \to A \in d)$
39	38	imp	$⊢ ((d \in ω \land suc A \in ω) \land suc A \subseteq d) \to A \in d$
40		eleq2w	$⊢ a = d \to (A \in a \leftrightarrow A \in d)$
41		suceq	$⊢ a = d \to suc a = suc d$
42	41	fveq2d	$⊢ a = d \to F (suc a) = F (suc d)$
43		fveq2	$⊢ a = d \to F (a) = F (d)$
44	42 43	eqeq12d	$⊢ a = d \to (F (suc a) = F (a) \leftrightarrow F (suc d) = F (d))$
45	40 44	imbi12d	$⊢ a = d \to ((A \in a \to F (suc a) = F (a)) \leftrightarrow (A \in d \to F (suc d) = F (d)))$
46	45	rspcv	$⊢ d \in ω \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to (A \in d \to F (suc d) = F (d)))$
47	46	com23	$⊢ d \in ω \to (A \in d \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc d) = F (d)))$
48	47	ad2antrr	$⊢ ((d \in ω \land suc A \in ω) \land suc A \subseteq d) \to (A \in d \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc d) = F (d)))$
49	39 48	mpd	$⊢ ((d \in ω \land suc A \in ω) \land suc A \subseteq d) \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc d) = F (d))$
50		eqtr3	$⊢ (F (suc A) = F (d) \land F (suc d) = F (d)) \to F (suc A) = F (suc d)$
51	50	expcom	$⊢ F (suc d) = F (d) \to (F (suc A) = F (d) \to F (suc A) = F (suc d))$
52	49 51	syl6	$⊢ ((d \in ω \land suc A \in ω) \land suc A \subseteq d) \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to (F (suc A) = F (d) \to F (suc A) = F (suc d)))$
53	52	a2d	$⊢ ((d \in ω \land suc A \in ω) \land suc A \subseteq d) \to ((\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (d)) \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (suc d)))$
54	21 24 27 30 32 53	findsg	$⊢ ((c \in ω \land suc A \in ω) \land suc A \subseteq c) \to (\forall a \in ω (A \in a \to F (suc a) = F (a)) \to F (suc A) = F (c))$
55	54	impr	$⊢ ((c \in ω \land suc A \in ω) \land (suc A \subseteq c \land \forall a \in ω (A \in a \to F (suc a) = F (a)))) \to F (suc A) = F (c)$
56	15 16 17 18 55	syl22anc	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land suc A \subseteq c) \to F (suc A) = F (c)$
57		eqimss	$⊢ F (suc A) = F (c) \to F (suc A) \subseteq F (c)$
58	56 57	syl	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land suc A \subseteq c) \to F (suc A) \subseteq F (c)$
59	6	ad3antlr	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land c \subseteq suc A) \to suc A \in ω$
60		simplrr	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land c \subseteq suc A) \to c \in ω$
61		simpr	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land c \subseteq suc A) \to c \subseteq suc A$
62		simplll	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land c \subseteq suc A) \to φ$
63	1 2 3	isf32lem1	$⊢ ((suc A \in ω \land c \in ω) \land (c \subseteq suc A \land φ)) \to F (suc A) \subseteq F (c)$
64	59 60 61 62 63	syl22anc	$⊢ (((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \land c \subseteq suc A) \to F (suc A) \subseteq F (c)$
65		nnord	$⊢ suc A \in ω \to Ord suc A$
66	6 65	syl	$⊢ A \in ω \to Ord suc A$
67	66	ad2antlr	$⊢ ((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \to Ord suc A$
68		nnord	$⊢ c \in ω \to Ord c$
69	68	ad2antll	$⊢ ((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \to Ord c$
70		ordtri2or2	$⊢ (Ord suc A \land Ord c) \to (suc A \subseteq c \lor c \subseteq suc A)$
71	67 69 70	syl2anc	$⊢ ((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \to (suc A \subseteq c \lor c \subseteq suc A)$
72	58 64 71	mpjaodan	$⊢ ((φ \land A \in ω) \land (\forall a \in ω (A \in a \to F (suc a) = F (a)) \land c \in ω)) \to F (suc A) \subseteq F (c)$
73	72	anassrs	$⊢ (((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \land c \in ω) \to F (suc A) \subseteq F (c)$
74		sseq2	$⊢ F (c) = b \to (F (suc A) \subseteq F (c) \leftrightarrow F (suc A) \subseteq b)$
75	73 74	syl5ibcom	$⊢ (((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \land c \in ω) \to (F (c) = b \to F (suc A) \subseteq b)$
76	75	rexlimdva	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to (\exists c \in ω F (c) = b \to F (suc A) \subseteq b)$
77	14 76	sylbid	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to (b \in ran F \to F (suc A) \subseteq b)$
78	77	ralrimiv	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to \forall b \in ran F F (suc A) \subseteq b$
79		ssint	$⊢ F (suc A) \subseteq ⋂ ran F \leftrightarrow \forall b \in ran F F (suc A) \subseteq b$
80	78 79	sylibr	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to F (suc A) \subseteq ⋂ ran F$
81	11 80	eqssd	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to ⋂ ran F = F (suc A)$
82	81 9	eqeltrd	$⊢ ((φ \land A \in ω) \land \forall a \in ω (A \in a \to F (suc a) = F (a))) \to ⋂ ran F \in ran F$
83	4 82	mtand	$⊢ (φ \land A \in ω) \to \neg \forall a \in ω (A \in a \to F (suc a) = F (a))$
84		rexnal	$⊢ \exists a \in ω \neg (A \in a \to F (suc a) = F (a)) \leftrightarrow \neg \forall a \in ω (A \in a \to F (suc a) = F (a))$
85	83 84	sylibr	$⊢ (φ \land A \in ω) \to \exists a \in ω \neg (A \in a \to F (suc a) = F (a))$
86		suceq	$⊢ x = a \to suc x = suc a$
87	86	fveq2d	$⊢ x = a \to F (suc x) = F (suc a)$
88		fveq2	$⊢ x = a \to F (x) = F (a)$
89	87 88	sseq12d	$⊢ x = a \to (F (suc x) \subseteq F (x) \leftrightarrow F (suc a) \subseteq F (a))$
90	89	cbvralvw	$⊢ \forall x \in ω F (suc x) \subseteq F (x) \leftrightarrow \forall a \in ω F (suc a) \subseteq F (a)$
91	2 90	sylib	$⊢ φ \to \forall a \in ω F (suc a) \subseteq F (a)$
92	91	adantr	$⊢ (φ \land A \in ω) \to \forall a \in ω F (suc a) \subseteq F (a)$
93		pm4.61	$⊢ \neg (A \in a \to F (suc a) = F (a)) \leftrightarrow (A \in a \land \neg F (suc a) = F (a))$
94		dfpss2	$⊢ F (suc a) \subset F (a) \leftrightarrow (F (suc a) \subseteq F (a) \land \neg F (suc a) = F (a))$
95	94	simplbi2	$⊢ F (suc a) \subseteq F (a) \to (\neg F (suc a) = F (a) \to F (suc a) \subset F (a))$
96	95	anim2d	$⊢ F (suc a) \subseteq F (a) \to ((A \in a \land \neg F (suc a) = F (a)) \to (A \in a \land F (suc a) \subset F (a)))$
97	93 96	biimtrid	$⊢ F (suc a) \subseteq F (a) \to (\neg (A \in a \to F (suc a) = F (a)) \to (A \in a \land F (suc a) \subset F (a)))$
98	97	ralimi	$⊢ \forall a \in ω F (suc a) \subseteq F (a) \to \forall a \in ω (\neg (A \in a \to F (suc a) = F (a)) \to (A \in a \land F (suc a) \subset F (a)))$
99		rexim	$⊢ \forall a \in ω (\neg (A \in a \to F (suc a) = F (a)) \to (A \in a \land F (suc a) \subset F (a))) \to (\exists a \in ω \neg (A \in a \to F (suc a) = F (a)) \to \exists a \in ω (A \in a \land F (suc a) \subset F (a)))$
100	92 98 99	3syl	$⊢ (φ \land A \in ω) \to (\exists a \in ω \neg (A \in a \to F (suc a) = F (a)) \to \exists a \in ω (A \in a \land F (suc a) \subset F (a)))$
101	85 100	mpd	$⊢ (φ \land A \in ω) \to \exists a \in ω (A \in a \land F (suc a) \subset F (a))$

Metamath Proof Explorer

Theorem isf32lem2

Proof