pthdlem2lem

	Ref	Expression
Hypotheses	pthd.p	$⊢ φ \to P \in Word V$
	pthd.r	$⊢ R = \|P\| - 1$
	pthd.s	$⊢ φ \to \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
Assertion	pthdlem2lem	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to P (I) \notin P [(1 ..^R)]$

Proof

Step	Hyp	Ref	Expression
1		pthd.p	$⊢ φ \to P \in Word V$
2		pthd.r	$⊢ R = \|P\| - 1$
3		pthd.s	$⊢ φ \to \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
4	3	3ad2ant1	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j))$
5		ralcom	$⊢ \forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j)) \leftrightarrow \forall j \in (1 ..^R) \forall i \in (0 ..^\|P\|) (i \neq j \to P (i) \neq P (j))$
6		elfzo1	$⊢ j \in (1 ..^R) \leftrightarrow (j \in ℕ \land R \in ℕ \land j < R)$
7		nnne0	$⊢ j \in ℕ \to j \neq 0$
8	7	necomd	$⊢ j \in ℕ \to 0 \neq j$
9	8	3ad2ant1	$⊢ (j \in ℕ \land R \in ℕ \land j < R) \to 0 \neq j$
10	6 9	sylbi	$⊢ j \in (1 ..^R) \to 0 \neq j$
11	10	adantl	$⊢ (\|P\| \in ℕ \land j \in (1 ..^R)) \to 0 \neq j$
12		neeq1	$⊢ I = 0 \to (I \neq j \leftrightarrow 0 \neq j)$
13	11 12	imbitrrid	$⊢ I = 0 \to ((\|P\| \in ℕ \land j \in (1 ..^R)) \to I \neq j)$
14	13	expd	$⊢ I = 0 \to (\|P\| \in ℕ \to (j \in (1 ..^R) \to I \neq j))$
15		nnre	$⊢ j \in ℕ \to j \in ℝ$
16	15	adantr	$⊢ (j \in ℕ \land R \in ℕ) \to j \in ℝ$
17		nnre	$⊢ R \in ℕ \to R \in ℝ$
18	17	adantl	$⊢ (j \in ℕ \land R \in ℕ) \to R \in ℝ$
19	16 18	ltlend	$⊢ (j \in ℕ \land R \in ℕ) \to (j < R \leftrightarrow (j \leq R \land R \neq j))$
20		simpr	$⊢ (j \leq R \land R \neq j) \to R \neq j$
21	19 20	syl6bi	$⊢ (j \in ℕ \land R \in ℕ) \to (j < R \to R \neq j)$
22	21	3impia	$⊢ (j \in ℕ \land R \in ℕ \land j < R) \to R \neq j$
23	6 22	sylbi	$⊢ j \in (1 ..^R) \to R \neq j$
24	23	adantl	$⊢ (\|P\| \in ℕ \land j \in (1 ..^R)) \to R \neq j$
25		neeq1	$⊢ I = R \to (I \neq j \leftrightarrow R \neq j)$
26	24 25	imbitrrid	$⊢ I = R \to ((\|P\| \in ℕ \land j \in (1 ..^R)) \to I \neq j)$
27	26	expd	$⊢ I = R \to (\|P\| \in ℕ \to (j \in (1 ..^R) \to I \neq j))$
28	14 27	jaoi	$⊢ (I = 0 \lor I = R) \to (\|P\| \in ℕ \to (j \in (1 ..^R) \to I \neq j))$
29	28	impcom	$⊢ (\|P\| \in ℕ \land (I = 0 \lor I = R)) \to (j \in (1 ..^R) \to I \neq j)$
30	29	3adant1	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to (j \in (1 ..^R) \to I \neq j)$
31	30	imp	$⊢ ((φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \land j \in (1 ..^R)) \to I \neq j$
32		lbfzo0	$⊢ 0 \in (0 ..^\|P\|) \leftrightarrow \|P\| \in ℕ$
33	32	biimpri	$⊢ \|P\| \in ℕ \to 0 \in (0 ..^\|P\|)$
34		eleq1	$⊢ I = 0 \to (I \in (0 ..^\|P\|) \leftrightarrow 0 \in (0 ..^\|P\|))$
35	33 34	imbitrrid	$⊢ I = 0 \to (\|P\| \in ℕ \to I \in (0 ..^\|P\|))$
36		fzo0end	$⊢ \|P\| \in ℕ \to \|P\| - 1 \in (0 ..^\|P\|)$
37	2 36	eqeltrid	$⊢ \|P\| \in ℕ \to R \in (0 ..^\|P\|)$
38		eleq1	$⊢ I = R \to (I \in (0 ..^\|P\|) \leftrightarrow R \in (0 ..^\|P\|))$
39	37 38	imbitrrid	$⊢ I = R \to (\|P\| \in ℕ \to I \in (0 ..^\|P\|))$
40	35 39	jaoi	$⊢ (I = 0 \lor I = R) \to (\|P\| \in ℕ \to I \in (0 ..^\|P\|))$
41	40	impcom	$⊢ (\|P\| \in ℕ \land (I = 0 \lor I = R)) \to I \in (0 ..^\|P\|)$
42	41	3adant1	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to I \in (0 ..^\|P\|)$
43	42	adantr	$⊢ ((φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \land j \in (1 ..^R)) \to I \in (0 ..^\|P\|)$
44		neeq1	$⊢ i = I \to (i \neq j \leftrightarrow I \neq j)$
45		fveq2	$⊢ i = I \to P (i) = P (I)$
46	45	neeq1d	$⊢ i = I \to (P (i) \neq P (j) \leftrightarrow P (I) \neq P (j))$
47	44 46	imbi12d	$⊢ i = I \to ((i \neq j \to P (i) \neq P (j)) \leftrightarrow (I \neq j \to P (I) \neq P (j)))$
48	47	rspcv	$⊢ I \in (0 ..^\|P\|) \to (\forall i \in (0 ..^\|P\|) (i \neq j \to P (i) \neq P (j)) \to (I \neq j \to P (I) \neq P (j)))$
49	43 48	syl	$⊢ ((φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \land j \in (1 ..^R)) \to (\forall i \in (0 ..^\|P\|) (i \neq j \to P (i) \neq P (j)) \to (I \neq j \to P (I) \neq P (j)))$
50	31 49	mpid	$⊢ ((φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \land j \in (1 ..^R)) \to (\forall i \in (0 ..^\|P\|) (i \neq j \to P (i) \neq P (j)) \to P (I) \neq P (j))$
51		nesym	$⊢ P (I) \neq P (j) \leftrightarrow \neg P (j) = P (I)$
52	50 51	imbitrdi	$⊢ ((φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \land j \in (1 ..^R)) \to (\forall i \in (0 ..^\|P\|) (i \neq j \to P (i) \neq P (j)) \to \neg P (j) = P (I))$
53	52	ralimdva	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to (\forall j \in (1 ..^R) \forall i \in (0 ..^\|P\|) (i \neq j \to P (i) \neq P (j)) \to \forall j \in (1 ..^R) \neg P (j) = P (I))$
54	5 53	biimtrid	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to (\forall i \in (0 ..^\|P\|) \forall j \in (1 ..^R) (i \neq j \to P (i) \neq P (j)) \to \forall j \in (1 ..^R) \neg P (j) = P (I))$
55	4 54	mpd	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to \forall j \in (1 ..^R) \neg P (j) = P (I)$
56		ralnex	$⊢ \forall j \in (1 ..^R) \neg P (j) = P (I) \leftrightarrow \neg \exists j \in (1 ..^R) P (j) = P (I)$
57	55 56	sylib	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to \neg \exists j \in (1 ..^R) P (j) = P (I)$
58		wrdf	$⊢ P \in Word V \to P : (0 ..^\|P\|) ⟶ V$
59		ffun	$⊢ P : (0 ..^\|P\|) ⟶ V \to Fun P$
60	1 58 59	3syl	$⊢ φ \to Fun P$
61	60	3ad2ant1	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to Fun P$
62		fvelima	$⊢ (Fun P \land P (I) \in P [(1 ..^R)]) \to \exists j \in (1 ..^R) P (j) = P (I)$
63	62	ex	$⊢ Fun P \to (P (I) \in P [(1 ..^R)] \to \exists j \in (1 ..^R) P (j) = P (I))$
64	61 63	syl	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to (P (I) \in P [(1 ..^R)] \to \exists j \in (1 ..^R) P (j) = P (I))$
65	57 64	mtod	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to \neg P (I) \in P [(1 ..^R)]$
66		df-nel	$⊢ P (I) \notin P [(1 ..^R)] \leftrightarrow \neg P (I) \in P [(1 ..^R)]$
67	65 66	sylibr	$⊢ (φ \land \|P\| \in ℕ \land (I = 0 \lor I = R)) \to P (I) \notin P [(1 ..^R)]$

Metamath Proof Explorer

Theorem pthdlem2lem

Proof