infpssrlem4

	Ref	Expression
Hypotheses	infpssrlem.a	$⊢ φ \to B \subseteq A$
	infpssrlem.c	$⊢ φ \to F : B \underset{1-1 onto}{⟶} A$
	infpssrlem.d	$⊢ φ \to C \in (A ∖ B)$
	infpssrlem.e	$⊢ G = {rec (F^{-1}, C) ↾}_{ω}$
Assertion	infpssrlem4	$⊢ (φ \land M \in ω \land N \in M) \to G (M) \neq G (N)$

Proof

Step	Hyp	Ref	Expression
1		infpssrlem.a	$⊢ φ \to B \subseteq A$
2		infpssrlem.c	$⊢ φ \to F : B \underset{1-1 onto}{⟶} A$
3		infpssrlem.d	$⊢ φ \to C \in (A ∖ B)$
4		infpssrlem.e	$⊢ G = {rec (F^{-1}, C) ↾}_{ω}$
5		fveq2	$⊢ c = \emptyset \to G (c) = G (\emptyset)$
6	5	neeq1d	$⊢ c = \emptyset \to (G (c) \neq G (b) \leftrightarrow G (\emptyset) \neq G (b))$
7	6	raleqbi1dv	$⊢ c = \emptyset \to (\forall b \in c G (c) \neq G (b) \leftrightarrow \forall b \in \emptyset G (\emptyset) \neq G (b))$
8	7	imbi2d	$⊢ c = \emptyset \to ((φ \to \forall b \in c G (c) \neq G (b)) \leftrightarrow (φ \to \forall b \in \emptyset G (\emptyset) \neq G (b)))$
9		fveq2	$⊢ c = d \to G (c) = G (d)$
10	9	neeq1d	$⊢ c = d \to (G (c) \neq G (b) \leftrightarrow G (d) \neq G (b))$
11	10	raleqbi1dv	$⊢ c = d \to (\forall b \in c G (c) \neq G (b) \leftrightarrow \forall b \in d G (d) \neq G (b))$
12	11	imbi2d	$⊢ c = d \to ((φ \to \forall b \in c G (c) \neq G (b)) \leftrightarrow (φ \to \forall b \in d G (d) \neq G (b)))$
13		fveq2	$⊢ c = suc d \to G (c) = G (suc d)$
14	13	neeq1d	$⊢ c = suc d \to (G (c) \neq G (b) \leftrightarrow G (suc d) \neq G (b))$
15	14	raleqbi1dv	$⊢ c = suc d \to (\forall b \in c G (c) \neq G (b) \leftrightarrow \forall b \in suc d G (suc d) \neq G (b))$
16	15	imbi2d	$⊢ c = suc d \to ((φ \to \forall b \in c G (c) \neq G (b)) \leftrightarrow (φ \to \forall b \in suc d G (suc d) \neq G (b)))$
17		fveq2	$⊢ c = M \to G (c) = G (M)$
18	17	neeq1d	$⊢ c = M \to (G (c) \neq G (b) \leftrightarrow G (M) \neq G (b))$
19	18	raleqbi1dv	$⊢ c = M \to (\forall b \in c G (c) \neq G (b) \leftrightarrow \forall b \in M G (M) \neq G (b))$
20	19	imbi2d	$⊢ c = M \to ((φ \to \forall b \in c G (c) \neq G (b)) \leftrightarrow (φ \to \forall b \in M G (M) \neq G (b)))$
21		ral0	$⊢ \forall b \in \emptyset G (\emptyset) \neq G (b)$
22	21	a1i	$⊢ φ \to \forall b \in \emptyset G (\emptyset) \neq G (b)$
23		f1ocnv	$⊢ F : B \underset{1-1 onto}{⟶} A \to F^{-1} : A \underset{1-1 onto}{⟶} B$
24		f1of	$⊢ F^{-1} : A \underset{1-1 onto}{⟶} B \to F^{-1} : A ⟶ B$
25	2 23 24	3syl	$⊢ φ \to F^{-1} : A ⟶ B$
26	25	adantl	$⊢ (d \in ω \land φ) \to F^{-1} : A ⟶ B$
27	1 2 3 4	infpssrlem3	$⊢ φ \to G : ω ⟶ A$
28	27	ffvelcdmda	$⊢ (φ \land d \in ω) \to G (d) \in A$
29	28	ancoms	$⊢ (d \in ω \land φ) \to G (d) \in A$
30	26 29	ffvelcdmd	$⊢ (d \in ω \land φ) \to F^{-1} (G (d)) \in B$
31	3	eldifbd	$⊢ φ \to \neg C \in B$
32	31	adantl	$⊢ (d \in ω \land φ) \to \neg C \in B$
33		nelne2	$⊢ (F^{-1} (G (d)) \in B \land \neg C \in B) \to F^{-1} (G (d)) \neq C$
34	30 32 33	syl2anc	$⊢ (d \in ω \land φ) \to F^{-1} (G (d)) \neq C$
35	1 2 3 4	infpssrlem2	$⊢ d \in ω \to G (suc d) = F^{-1} (G (d))$
36	35	adantr	$⊢ (d \in ω \land φ) \to G (suc d) = F^{-1} (G (d))$
37	1 2 3 4	infpssrlem1	$⊢ φ \to G (\emptyset) = C$
38	37	adantl	$⊢ (d \in ω \land φ) \to G (\emptyset) = C$
39	34 36 38	3netr4d	$⊢ (d \in ω \land φ) \to G (suc d) \neq G (\emptyset)$
40	39	3adant3	$⊢ (d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \to G (suc d) \neq G (\emptyset)$
41	5	neeq2d	$⊢ c = \emptyset \to (G (suc d) \neq G (c) \leftrightarrow G (suc d) \neq G (\emptyset))$
42	40 41	imbitrrid	$⊢ c = \emptyset \to ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \to G (suc d) \neq G (c))$
43	42	adantrd	$⊢ c = \emptyset \to (((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to G (suc d) \neq G (c))$
44		simpr	$⊢ (d \in ω \land c \in suc d) \to c \in suc d$
45		peano2	$⊢ d \in ω \to suc d \in ω$
46	45	adantr	$⊢ (d \in ω \land c \in suc d) \to suc d \in ω$
47		elnn	$⊢ (c \in suc d \land suc d \in ω) \to c \in ω$
48	44 46 47	syl2anc	$⊢ (d \in ω \land c \in suc d) \to c \in ω$
49	48	3ad2antl1	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to c \in ω$
50	49	adantl	$⊢ (c \neq \emptyset \land ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d)) \to c \in ω$
51		simpl	$⊢ (c \neq \emptyset \land ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d)) \to c \neq \emptyset$
52		nnsuc	$⊢ (c \in ω \land c \neq \emptyset) \to \exists b \in ω c = suc b$
53	50 51 52	syl2anc	$⊢ (c \neq \emptyset \land ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d)) \to \exists b \in ω c = suc b$
54		nfv	$⊢ Ⅎ b d \in ω$
55		nfv	$⊢ Ⅎ b φ$
56		nfra1	$⊢ Ⅎ b \forall b \in d G (d) \neq G (b)$
57	54 55 56	nf3an	$⊢ Ⅎ b (d \in ω \land φ \land \forall b \in d G (d) \neq G (b))$
58		nfv	$⊢ Ⅎ b c \in suc d$
59	57 58	nfan	$⊢ Ⅎ b ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d)$
60		nfv	$⊢ Ⅎ b G (suc d) \neq G (c)$
61		simpl3	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land (suc b \in suc d \land b \in ω)) \to \forall b \in d G (d) \neq G (b)$
62		simpr	$⊢ (d \in ω \land suc b \in suc d) \to suc b \in suc d$
63		nnord	$⊢ d \in ω \to Ord d$
64	63	adantr	$⊢ (d \in ω \land suc b \in suc d) \to Ord d$
65		ordsucelsuc	$⊢ Ord d \to (b \in d \leftrightarrow suc b \in suc d)$
66	64 65	syl	$⊢ (d \in ω \land suc b \in suc d) \to (b \in d \leftrightarrow suc b \in suc d)$
67	62 66	mpbird	$⊢ (d \in ω \land suc b \in suc d) \to b \in d$
68	67	3ad2antl1	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land suc b \in suc d) \to b \in d$
69	68	adantrr	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land (suc b \in suc d \land b \in ω)) \to b \in d$
70		rsp	$⊢ \forall b \in d G (d) \neq G (b) \to (b \in d \to G (d) \neq G (b))$
71	61 69 70	sylc	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land (suc b \in suc d \land b \in ω)) \to G (d) \neq G (b)$
72		f1of1	$⊢ F^{-1} : A \underset{1-1 onto}{⟶} B \to F^{-1} : A \underset{1-1}{⟶} B$
73	2 23 72	3syl	$⊢ φ \to F^{-1} : A \underset{1-1}{⟶} B$
74	73	ad2antlr	$⊢ ((d \in ω \land φ) \land b \in ω) \to F^{-1} : A \underset{1-1}{⟶} B$
75	29	adantr	$⊢ ((d \in ω \land φ) \land b \in ω) \to G (d) \in A$
76	27	ffvelcdmda	$⊢ (φ \land b \in ω) \to G (b) \in A$
77	76	adantll	$⊢ ((d \in ω \land φ) \land b \in ω) \to G (b) \in A$
78		f1fveq	$⊢ (F^{-1} : A \underset{1-1}{⟶} B \land (G (d) \in A \land G (b) \in A)) \to (F^{-1} (G (d)) = F^{-1} (G (b)) \leftrightarrow G (d) = G (b))$
79	74 75 77 78	syl12anc	$⊢ ((d \in ω \land φ) \land b \in ω) \to (F^{-1} (G (d)) = F^{-1} (G (b)) \leftrightarrow G (d) = G (b))$
80	79	necon3bid	$⊢ ((d \in ω \land φ) \land b \in ω) \to (F^{-1} (G (d)) \neq F^{-1} (G (b)) \leftrightarrow G (d) \neq G (b))$
81	80	biimprd	$⊢ ((d \in ω \land φ) \land b \in ω) \to (G (d) \neq G (b) \to F^{-1} (G (d)) \neq F^{-1} (G (b)))$
82	35	adantr	$⊢ (d \in ω \land b \in ω) \to G (suc d) = F^{-1} (G (d))$
83	1 2 3 4	infpssrlem2	$⊢ b \in ω \to G (suc b) = F^{-1} (G (b))$
84	83	adantl	$⊢ (d \in ω \land b \in ω) \to G (suc b) = F^{-1} (G (b))$
85	82 84	neeq12d	$⊢ (d \in ω \land b \in ω) \to (G (suc d) \neq G (suc b) \leftrightarrow F^{-1} (G (d)) \neq F^{-1} (G (b)))$
86	85	adantlr	$⊢ ((d \in ω \land φ) \land b \in ω) \to (G (suc d) \neq G (suc b) \leftrightarrow F^{-1} (G (d)) \neq F^{-1} (G (b)))$
87	81 86	sylibrd	$⊢ ((d \in ω \land φ) \land b \in ω) \to (G (d) \neq G (b) \to G (suc d) \neq G (suc b))$
88	87	adantrl	$⊢ ((d \in ω \land φ) \land (suc b \in suc d \land b \in ω)) \to (G (d) \neq G (b) \to G (suc d) \neq G (suc b))$
89	88	3adantl3	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land (suc b \in suc d \land b \in ω)) \to (G (d) \neq G (b) \to G (suc d) \neq G (suc b))$
90	71 89	mpd	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land (suc b \in suc d \land b \in ω)) \to G (suc d) \neq G (suc b)$
91	90	expr	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land suc b \in suc d) \to (b \in ω \to G (suc d) \neq G (suc b))$
92		eleq1	$⊢ c = suc b \to (c \in suc d \leftrightarrow suc b \in suc d)$
93	92	anbi2d	$⊢ c = suc b \to (((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \leftrightarrow ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land suc b \in suc d))$
94		fveq2	$⊢ c = suc b \to G (c) = G (suc b)$
95	94	neeq2d	$⊢ c = suc b \to (G (suc d) \neq G (c) \leftrightarrow G (suc d) \neq G (suc b))$
96	95	imbi2d	$⊢ c = suc b \to ((b \in ω \to G (suc d) \neq G (c)) \leftrightarrow (b \in ω \to G (suc d) \neq G (suc b)))$
97	93 96	imbi12d	$⊢ c = suc b \to ((((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to (b \in ω \to G (suc d) \neq G (c))) \leftrightarrow (((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land suc b \in suc d) \to (b \in ω \to G (suc d) \neq G (suc b))))$
98	91 97	mpbiri	$⊢ c = suc b \to (((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to (b \in ω \to G (suc d) \neq G (c)))$
99	98	com3l	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to (b \in ω \to (c = suc b \to G (suc d) \neq G (c)))$
100	59 60 99	rexlimd	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to (\exists b \in ω c = suc b \to G (suc d) \neq G (c))$
101	100	adantl	$⊢ (c \neq \emptyset \land ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d)) \to (\exists b \in ω c = suc b \to G (suc d) \neq G (c))$
102	53 101	mpd	$⊢ (c \neq \emptyset \land ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d)) \to G (suc d) \neq G (c)$
103	102	ex	$⊢ c \neq \emptyset \to (((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to G (suc d) \neq G (c))$
104	43 103	pm2.61ine	$⊢ ((d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \land c \in suc d) \to G (suc d) \neq G (c)$
105	104	ralrimiva	$⊢ (d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \to \forall c \in suc d G (suc d) \neq G (c)$
106		fveq2	$⊢ c = b \to G (c) = G (b)$
107	106	neeq2d	$⊢ c = b \to (G (suc d) \neq G (c) \leftrightarrow G (suc d) \neq G (b))$
108	107	cbvralvw	$⊢ \forall c \in suc d G (suc d) \neq G (c) \leftrightarrow \forall b \in suc d G (suc d) \neq G (b)$
109	105 108	sylib	$⊢ (d \in ω \land φ \land \forall b \in d G (d) \neq G (b)) \to \forall b \in suc d G (suc d) \neq G (b)$
110	109	3exp	$⊢ d \in ω \to (φ \to (\forall b \in d G (d) \neq G (b) \to \forall b \in suc d G (suc d) \neq G (b)))$
111	110	a2d	$⊢ d \in ω \to ((φ \to \forall b \in d G (d) \neq G (b)) \to (φ \to \forall b \in suc d G (suc d) \neq G (b)))$
112	8 12 16 20 22 111	finds	$⊢ M \in ω \to (φ \to \forall b \in M G (M) \neq G (b))$
113	112	impcom	$⊢ (φ \land M \in ω) \to \forall b \in M G (M) \neq G (b)$
114		fveq2	$⊢ b = N \to G (b) = G (N)$
115	114	neeq2d	$⊢ b = N \to (G (M) \neq G (b) \leftrightarrow G (M) \neq G (N))$
116	115	rspccv	$⊢ \forall b \in M G (M) \neq G (b) \to (N \in M \to G (M) \neq G (N))$
117	113 116	syl	$⊢ (φ \land M \in ω) \to (N \in M \to G (M) \neq G (N))$
118	117	3impia	$⊢ (φ \land M \in ω \land N \in M) \to G (M) \neq G (N)$

Metamath Proof Explorer

Theorem infpssrlem4

Proof