Theorem bnj594 14229

Description: Technical lemma of bnj75 14239. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem).

Hypotheses

Ref	Expression
bnj594.1	|- (ph <-> (f` (/)) = pred(x, A, R))
bnj594.2	|- (ps <-> A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
bnj594.3	|- (ch <-> (f Fn n /\ ph /\ ps))
bnj594.7	|- D = (om \ {(/)})
bnj594.9	|- (ph' <-> (g` (/)) = pred(x, A, R))
bnj594.10	|- (ps' <-> A.i e. om (suc i e. n -> (g` suc i) = U_y e. (g` i) pred(y, A, R)))
bnj594.11	|- (ch' <-> (g Fn n /\ ph' /\ ps'))
bnj594.15	|- (th <-> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
bnj594.16	|- ([k / j]th <-> ((n e. D /\ ch /\ ch') -> (f` k) = (g` k)))
bnj594.17	|- (ta <-> A.k e. n (k _E j -> [k / j]th))

Assertion

Ref	Expression
bnj594	|- ((j e. n /\ ta) -> th)

Distinct variable groups:   A,i,k   D,k   R,i,k   ch,k   k,ch'   f,i,k,y   g,i,k,y   i,n,k   j,k

Proof of Theorem bnj594

Step	Hyp	Ref	Expression
1		bnj594.3	. . . . . . . . 9 |- (ch <-> (f Fn n /\ ph /\ ps))
2	1	simp2bi 1164	. . . . . . . 8 |- (ch -> ph)
3		bnj594.1	. . . . . . . 8 |- (ph <-> (f` (/)) = pred(x, A, R))
4	2, 3	sylib 263	. . . . . . 7 |- (ch -> (f` (/)) = pred(x, A, R))
5		bnj594.11	. . . . . . . . 9 |- (ch' <-> (g Fn n /\ ph' /\ ps'))
6	5	simp2bi 1164	. . . . . . . 8 |- (ch' -> ph')
7		bnj594.9	. . . . . . . 8 |- (ph' <-> (g` (/)) = pred(x, A, R))
8	6, 7	sylib 263	. . . . . . 7 |- (ch' -> (g` (/)) = pred(x, A, R))
9		eqtr3 2189	. . . . . . 7 |- (((f` (/)) = pred(x, A, R) /\ (g` (/)) = pred(x, A, R)) -> (f` (/)) = (g` (/)))
10	4, 8, 9	syl2an 699	. . . . . 6 |- ((ch /\ ch') -> (f` (/)) = (g` (/)))
11	10	3adant1 1166	. . . . 5 |- ((n e. D /\ ch /\ ch') -> (f` (/)) = (g` (/)))
12		fveq2 4804	. . . . . 6 |- (j = (/) -> (f` j) = (f` (/)))
13		fveq2 4804	. . . . . 6 |- (j = (/) -> (g` j) = (g` (/)))
14	12, 13	eqeq12d 2184	. . . . 5 |- (j = (/) -> ((f` j) = (g` j) <-> (f` (/)) = (g` (/))))
15	11, 14	syl5ibr 278	. . . 4 |- (j = (/) -> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
16		bnj594.15	. . . 4 |- (th <-> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
17	15, 16	sylibr 264	. . 3 |- (j = (/) -> th)
18	17	a1d 18	. 2 |- (j = (/) -> ((j e. n /\ ta) -> th))
19		bnj253 13070	. . . . . 6 |- ((n e. D /\ n e. D /\ ch /\ ch') <-> ((n e. D /\ n e. D) /\ ch /\ ch'))
20		bnj252 13069	. . . . . 6 |- ((n e. D /\ n e. D /\ ch /\ ch') <-> (n e. D /\ (n e. D /\ ch /\ ch')))
21		anidm 720	. . . . . . 7 |- ((n e. D /\ n e. D) <-> n e. D)
22	21	3anbi1i 1336	. . . . . 6 |- (((n e. D /\ n e. D) /\ ch /\ ch') <-> (n e. D /\ ch /\ ch'))
23	19, 20, 22	3bitr3i 338	. . . . 5 |- ((n e. D /\ (n e. D /\ ch /\ ch')) <-> (n e. D /\ ch /\ ch'))
24		df-bnj17 13009	. . . . . . . . . 10 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) <-> ((j =/= (/) /\ j e. n /\ n e. D) /\ ta))
25		ax-17 1634	. . . . . . . . . . 11 |- ((j =/= (/) /\ j e. n /\ n e. D) -> A.k(j =/= (/) /\ j e. n /\ n e. D))
26		bnj594.17	. . . . . . . . . . . 12 |- (ta <-> A.k e. n (k _E j -> [k / j]th))
27	26	bnj1095 13844	. . . . . . . . . . 11 |- (ta -> A.kta)
28	25, 27	hban 1674	. . . . . . . . . 10 |- (((j =/= (/) /\ j e. n /\ n e. D) /\ ta) -> A.k((j =/= (/) /\ j e. n /\ n e. D) /\ ta))
29	24, 28	bnj572 13475	. . . . . . . . 9 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) -> A.k(j =/= (/) /\ j e. n /\ n e. D /\ ta))
30		bnj170 13023	. . . . . . . . . . . 12 |- ((j =/= (/) /\ j e. n /\ n e. D) <-> ((j e. n /\ n e. D) /\ j =/= (/)))
31		bnj594.7	. . . . . . . . . . . . . . 15 |- D = (om \ {(/)})
32	31	bnj923 13759	. . . . . . . . . . . . . 14 |- (n e. D -> n e. om)
33		elnn 4128	. . . . . . . . . . . . . 14 |- ((j e. n /\ n e. om) -> j e. om)
34	32, 33	sylan2 696	. . . . . . . . . . . . 13 |- ((j e. n /\ n e. D) -> j e. om)
35	34	anim1i 634	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D) /\ j =/= (/)) -> (j e. om /\ j =/= (/)))
36	30, 35	sylbi 237	. . . . . . . . . . 11 |- ((j =/= (/) /\ j e. n /\ n e. D) -> (j e. om /\ j =/= (/)))
37		nnsuc 4135	. . . . . . . . . . 11 |- ((j e. om /\ j =/= (/)) -> E.k e. om j = suc k)
38		rexex 2435	. . . . . . . . . . 11 |- (E.k e. om j = suc k -> E.k j = suc k)
39	36, 37, 38	3syl 38	. . . . . . . . . 10 |- ((j =/= (/) /\ j e. n /\ n e. D) -> E.k j = suc k)
40	39	bnj721 13588	. . . . . . . . 9 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) -> E.k j = suc k)
41	29, 40	bnj596 13487	. . . . . . . 8 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) -> E.k((j =/= (/) /\ j e. n /\ n e. D /\ ta) /\ j = suc k))
42		bnj667 13531	. . . . . . . . . . 11 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) -> (j e. n /\ n e. D /\ ta))
43	42	anim1i 634	. . . . . . . . . 10 |- (((j =/= (/) /\ j e. n /\ n e. D /\ ta) /\ j = suc k) -> ((j e. n /\ n e. D /\ ta) /\ j = suc k))
44		bnj258 13075	. . . . . . . . . 10 |- ((j e. n /\ n e. D /\ j = suc k /\ ta) <-> ((j e. n /\ n e. D /\ ta) /\ j = suc k))
45	43, 44	sylibr 264	. . . . . . . . 9 |- (((j =/= (/) /\ j e. n /\ n e. D /\ ta) /\ j = suc k) -> (j e. n /\ n e. D /\ j = suc k /\ ta))
46		df-bnj17 13009	. . . . . . . . . . . . . . 15 |- ((j e. n /\ n e. D /\ j = suc k /\ ta) <-> ((j e. n /\ n e. D /\ j = suc k) /\ ta))
47		bnj219 13442	. . . . . . . . . . . . . . . . . 18 |- (j = suc k -> k _E j)
48	47	3ad2ant3 1171	. . . . . . . . . . . . . . . . 17 |- ((j e. n /\ n e. D /\ j = suc k) -> k _E j)
49	48	adantr 543	. . . . . . . . . . . . . . . 16 |- (((j e. n /\ n e. D /\ j = suc k) /\ ta) -> k _E j)
50		visset 2572	. . . . . . . . . . . . . . . . . . 19 |- k e. _V
51	50	bnj216 13439	. . . . . . . . . . . . . . . . . 18 |- (j = suc k -> k e. j)
52		bnj177 13030	. . . . . . . . . . . . . . . . . . 19 |- ((j e. n /\ n e. D /\ k e. j) <-> (n e. D /\ (k e. j /\ j e. n)))
53	31	eleq2i 2237	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. D <-> n e. (om \ {(/)}))
54	53	biimpi 236	. . . . . . . . . . . . . . . . . . . . . 22 |- (n e. D -> n e. (om \ {(/)}))
55		eldifi 2981	. . . . . . . . . . . . . . . . . . . . . 22 |- (n e. (om \ {(/)}) -> n e. om)
56		nnord 4126	. . . . . . . . . . . . . . . . . . . . . 22 |- (n e. om -> Ord n)
57	54, 55, 56	3syl 38	. . . . . . . . . . . . . . . . . . . . 21 |- (n e. D -> Ord n)
58		ordtr1 3886	. . . . . . . . . . . . . . . . . . . . 21 |- (Ord n -> ((k e. j /\ j e. n) -> k e. n))
59	57, 58	syl 13	. . . . . . . . . . . . . . . . . . . 20 |- (n e. D -> ((k e. j /\ j e. n) -> k e. n))
60	59	imp 489	. . . . . . . . . . . . . . . . . . 19 |- ((n e. D /\ (k e. j /\ j e. n)) -> k e. n)
61	52, 60	sylbi 237	. . . . . . . . . . . . . . . . . 18 |- ((j e. n /\ n e. D /\ k e. j) -> k e. n)
62	51, 61	syl3an3 1412	. . . . . . . . . . . . . . . . 17 |- ((j e. n /\ n e. D /\ j = suc k) -> k e. n)
63		ra4 2436	. . . . . . . . . . . . . . . . . 18 |- (A.k e. n (k _E j -> [k / j]th) -> (k e. n -> (k _E j -> [k / j]th)))
64	26, 63	sylbi 237	. . . . . . . . . . . . . . . . 17 |- (ta -> (k e. n -> (k _E j -> [k / j]th)))
65	62, 64	mpan9 690	. . . . . . . . . . . . . . . 16 |- (((j e. n /\ n e. D /\ j = suc k) /\ ta) -> (k _E j -> [k / j]th))
66	49, 65	mpd 11	. . . . . . . . . . . . . . 15 |- (((j e. n /\ n e. D /\ j = suc k) /\ ta) -> [k / j]th)
67	46, 66	sylbi 237	. . . . . . . . . . . . . 14 |- ((j e. n /\ n e. D /\ j = suc k /\ ta) -> [k / j]th)
68	67	anim1i 634	. . . . . . . . . . . . 13 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> ([k / j]th /\ (n e. D /\ ch /\ ch')))
69		bnj252 13069	. . . . . . . . . . . . 13 |- (([k / j]th /\ n e. D /\ ch /\ ch') <-> ([k / j]th /\ (n e. D /\ ch /\ ch')))
70	68, 69	sylibr 264	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> ([k / j]th /\ n e. D /\ ch /\ ch'))
71		bnj446 13262	. . . . . . . . . . . . 13 |- (([k / j]th /\ n e. D /\ ch /\ ch') <-> ((n e. D /\ ch /\ ch') /\ [k / j]th))
72		bnj594.16	. . . . . . . . . . . . . 14 |- ([k / j]th <-> ((n e. D /\ ch /\ ch') -> (f` k) = (g` k)))
73		pm3.35 659	. . . . . . . . . . . . . 14 |- (((n e. D /\ ch /\ ch') /\ ((n e. D /\ ch /\ ch') -> (f` k) = (g` k))) -> (f` k) = (g` k))
74	72, 73	sylan2b 697	. . . . . . . . . . . . 13 |- (((n e. D /\ ch /\ ch') /\ [k / j]th) -> (f` k) = (g` k))
75	71, 74	sylbi 237	. . . . . . . . . . . 12 |- (([k / j]th /\ n e. D /\ ch /\ ch') -> (f` k) = (g` k))
76		iuneq1 3479	. . . . . . . . . . . 12 |- ((f` k) = (g` k) -> U_y e. (f` k) pred(y, A, R) = U_y e. (g` k) pred(y, A, R))
77	70, 75, 76	3syl 38	. . . . . . . . . . 11 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> U_y e. (f` k) pred(y, A, R) = U_y e. (g` k) pred(y, A, R))
78		bnj658 13522	. . . . . . . . . . . . 13 |- ((j e. n /\ n e. D /\ j = suc k /\ ta) -> (j e. n /\ n e. D /\ j = suc k))
79	1	simp3bi 1165	. . . . . . . . . . . . . 14 |- (ch -> ps)
80	5	simp3bi 1165	. . . . . . . . . . . . . 14 |- (ch' -> ps')
81	79, 80	bnj240 13058	. . . . . . . . . . . . 13 |- ((n e. D /\ ch /\ ch') -> (ps /\ ps'))
82	78, 81	anim12i 632	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> ((j e. n /\ n e. D /\ j = suc k) /\ (ps /\ ps')))
83		simpl 533	. . . . . . . . . . . . 13 |- ((ps /\ ps') -> ps)
84	83	anim2i 635	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D /\ j = suc k) /\ (ps /\ ps')) -> ((j e. n /\ n e. D /\ j = suc k) /\ ps))
85		simp3 1150	. . . . . . . . . . . . . 14 |- ((j e. n /\ n e. D /\ j = suc k) -> j = suc k)
86	85	anim1i 634	. . . . . . . . . . . . 13 |- (((j e. n /\ n e. D /\ j = suc k) /\ ps) -> (j = suc k /\ ps))
87		simpl1 1151	. . . . . . . . . . . . . 14 |- (((j e. n /\ n e. D /\ j = suc k) /\ (j = suc k /\ ps)) -> j e. n)
88		bnj178 13031	. . . . . . . . . . . . . . . 16 |- ((j e. n /\ n e. D /\ j = suc k) <-> (j = suc k /\ (j e. n /\ n e. D)))
89		elnn 4128	. . . . . . . . . . . . . . . . 17 |- ((k e. j /\ j e. om) -> k e. om)
90	51, 34, 89	syl2an 699	. . . . . . . . . . . . . . . 16 |- ((j = suc k /\ (j e. n /\ n e. D)) -> k e. om)
91	88, 90	sylbi 237	. . . . . . . . . . . . . . 15 |- ((j e. n /\ n e. D /\ j = suc k) -> k e. om)
92		bnj594.2	. . . . . . . . . . . . . . . . 17 |- (ps <-> A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
93	92	bnj222 14180	. . . . . . . . . . . . . . . 16 |- (ps <-> A.k e. om (suc k e. n -> (f` suc k) = U_y e. (f` k) pred(y, A, R)))
94	93	bnj590 14227	. . . . . . . . . . . . . . 15 |- ((j = suc k /\ ps) -> (k e. om -> (j e. n -> (f` j) = U_y e. (f` k) pred(y, A, R))))
95	91, 94	mpan9 690	. . . . . . . . . . . . . 14 |- (((j e. n /\ n e. D /\ j = suc k) /\ (j = suc k /\ ps)) -> (j e. n -> (f` j) = U_y e. (f` k) pred(y, A, R)))
96	87, 95	mpd 11	. . . . . . . . . . . . 13 |- (((j e. n /\ n e. D /\ j = suc k) /\ (j = suc k /\ ps)) -> (f` j) = U_y e. (f` k) pred(y, A, R))
97	86, 96	syldan 691	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D /\ j = suc k) /\ ps) -> (f` j) = U_y e. (f` k) pred(y, A, R))
98	82, 84, 97	3syl 38	. . . . . . . . . . 11 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> (f` j) = U_y e. (f` k) pred(y, A, R))
99		simpr 538	. . . . . . . . . . . . 13 |- ((ps /\ ps') -> ps')
100	99	anim2i 635	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D /\ j = suc k) /\ (ps /\ ps')) -> ((j e. n /\ n e. D /\ j = suc k) /\ ps'))
101	85	anim1i 634	. . . . . . . . . . . . 13 |- (((j e. n /\ n e. D /\ j = suc k) /\ ps') -> (j = suc k /\ ps'))
102		simpl1 1151	. . . . . . . . . . . . . 14 |- (((j e. n /\ n e. D /\ j = suc k) /\ (j = suc k /\ ps')) -> j e. n)
103		bnj594.10	. . . . . . . . . . . . . . . . 17 |- (ps' <-> A.i e. om (suc i e. n -> (g` suc i) = U_y e. (g` i) pred(y, A, R)))
104	103	bnj222 14180	. . . . . . . . . . . . . . . 16 |- (ps' <-> A.k e. om (suc k e. n -> (g` suc k) = U_y e. (g` k) pred(y, A, R)))
105	104	bnj590 14227	. . . . . . . . . . . . . . 15 |- ((j = suc k /\ ps') -> (k e. om -> (j e. n -> (g` j) = U_y e. (g` k) pred(y, A, R))))
106	91, 105	mpan9 690	. . . . . . . . . . . . . 14 |- (((j e. n /\ n e. D /\ j = suc k) /\ (j = suc k /\ ps')) -> (j e. n -> (g` j) = U_y e. (g` k) pred(y, A, R)))
107	102, 106	mpd 11	. . . . . . . . . . . . 13 |- (((j e. n /\ n e. D /\ j = suc k) /\ (j = suc k /\ ps')) -> (g` j) = U_y e. (g` k) pred(y, A, R))
108	101, 107	syldan 691	. . . . . . . . . . . 12 |- (((j e. n /\ n e. D /\ j = suc k) /\ ps') -> (g` j) = U_y e. (g` k) pred(y, A, R))
109	82, 100, 108	3syl 38	. . . . . . . . . . 11 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> (g` j) = U_y e. (g` k) pred(y, A, R))
110	77, 98, 109	3eqtr4d 2212	. . . . . . . . . 10 |- (((j e. n /\ n e. D /\ j = suc k /\ ta) /\ (n e. D /\ ch /\ ch')) -> (f` j) = (g` j))
111	110	ex 494	. . . . . . . . 9 |- ((j e. n /\ n e. D /\ j = suc k /\ ta) -> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
112	45, 111	syl 13	. . . . . . . 8 |- (((j =/= (/) /\ j e. n /\ n e. D /\ ta) /\ j = suc k) -> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
113	41, 112	bnj593 13486	. . . . . . 7 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) -> E.k((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
114		bnj258 13075	. . . . . . 7 |- ((j =/= (/) /\ j e. n /\ n e. D /\ ta) <-> ((j =/= (/) /\ j e. n /\ ta) /\ n e. D))
115		19.9v 1960	. . . . . . 7 |- (E.k((n e. D /\ ch /\ ch') -> (f` j) = (g` j)) <-> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
116	113, 114, 115	3imtr3i 328	. . . . . 6 |- (((j =/= (/) /\ j e. n /\ ta) /\ n e. D) -> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
117	116	expimpd 672	. . . . 5 |- ((j =/= (/) /\ j e. n /\ ta) -> ((n e. D /\ (n e. D /\ ch /\ ch')) -> (f` j) = (g` j)))
118	23, 117	syl5bir 272	. . . 4 |- ((j =/= (/) /\ j e. n /\ ta) -> ((n e. D /\ ch /\ ch') -> (f` j) = (g` j)))
119	118, 16	sylibr 264	. . 3 |- ((j =/= (/) /\ j e. n /\ ta) -> th)
120	119	3expib 1348	. 2 |- (j =/= (/) -> ((j e. n /\ ta) -> th))
121	18, 120	pm2.61ine 2368	1 |- ((j e. n /\ ta) -> th)

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  E.wex 1644  [wsbc 1843   =/= wne 2295  A.wral 2385  E.wrex 2386   \ cdif 2856  (/)c0 3114  {csn 3270  U_ciun 3468   class class class wbr 3539   _E cep 3774  Ord word 3842  suc csuc 3845  omcom 4117   Fn wfn 4158  ` cfv 4163   /\ syn-bnj17 13008   predsyn-bnj14 13012

This theorem is referenced by:  bnj580 14230

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-cnv 4167  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fv 4179  df-bnj17 13009

Copyright terms: Public domain