Theorem bnj605 30977

Description: Technical lemma. 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). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj605.5	|- ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )
bnj605.13	|- ( ph" <-> [. f / f ]. ph )
bnj605.14	|- ( ps" <-> [. f / f ]. ps )
bnj605.17	|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj605.19	|- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )
bnj605.28	|- f e. _V
bnj605.31	|- ( ch' <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
bnj605.32	|- ( ph" <-> ( f ` (/) ) = pred ( x , A , R ) )
bnj605.33	|- ( ps" <-> A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
bnj605.37	|- ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )
bnj605.38	|- ( ( th /\ m e. D /\ m _E n ) -> ch' )
bnj605.41	|- ( ( R FrSe A /\ ta /\ et ) -> f Fn n )
bnj605.42	|- ( ( R FrSe A /\ ta /\ et ) -> ph" )
bnj605.43	|- ( ( R FrSe A /\ ta /\ et ) -> ps" )

Assertion

Ref	Expression
bnj605	|- ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )

Distinct variable groups:   A, f, m   A, p, f   R, f, m   R, p   et, f   m, n   ph, m   ps, m   x, m   n, p   ph, p   ps, p   th, p   x, p

Allowed substitution hints:   ph( x, y, f, i, n)   ps( x, y, f, i, n)   ch( x, y, f, i, m, n, p)   th( x, y, f, i, m, n)   ta( x, y, f, i, m, n, p)   et( x, y, i, m, n, p)   A( x, y, i, n)   D( x, y, f, i, m, n, p)   R( x, y, i, n)   ph'( x, y, f, i, m, n, p)   ps'( x, y, f, i, m, n, p)   ch'( x, y, f, i, m, n, p)   ph"( x, y, f, i, m, n, p)   ps"( x, y, f, i, m, n, p)

Proof of Theorem bnj605

Step	Hyp	Ref	Expression
1		bnj605.37	. . . . 5 |- ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )
2	1	anim1i 592	. . . 4 |- ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> ( E. m E. p et /\ th ) )
3		nfv 1843	. . . . . . 7 |- F/ p th
4	3	19.41 2103	. . . . . 6 |- ( E. p ( et /\ th ) <-> ( E. p et /\ th ) )
5	4	exbii 1774	. . . . 5 |- ( E. m E. p ( et /\ th ) <-> E. m ( E. p et /\ th ) )
6		bnj605.5	. . . . . . . 8 |- ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )
7	6	bnj1095 30852	. . . . . . 7 |- ( th -> A. m th )
8	7	nf5i 2024	. . . . . 6 |- F/ m th
9	8	19.41 2103	. . . . 5 |- ( E. m ( E. p et /\ th ) <-> ( E. m E. p et /\ th ) )
10	5, 9	bitr2i 265	. . . 4 |- ( ( E. m E. p et /\ th ) <-> E. m E. p ( et /\ th ) )
11	2, 10	sylib 208	. . 3 |- ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> E. m E. p ( et /\ th ) )
12		bnj605.19	. . . . . . . . . 10 |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )
13	12	bnj1232 30874	. . . . . . . . 9 |- ( et -> m e. D )
14		bnj219 30801	. . . . . . . . . 10 |- ( n = suc m -> m _E n )
15	12, 14	bnj770 30833	. . . . . . . . 9 |- ( et -> m _E n )
16	13, 15	jca 554	. . . . . . . 8 |- ( et -> ( m e. D /\ m _E n ) )
17	16	anim1i 592	. . . . . . 7 |- ( ( et /\ th ) -> ( ( m e. D /\ m _E n ) /\ th ) )
18		bnj170 30764	. . . . . . 7 |- ( ( th /\ m e. D /\ m _E n ) <-> ( ( m e. D /\ m _E n ) /\ th ) )
19	17, 18	sylibr 224	. . . . . 6 |- ( ( et /\ th ) -> ( th /\ m e. D /\ m _E n ) )
20		bnj605.38	. . . . . 6 |- ( ( th /\ m e. D /\ m _E n ) -> ch' )
21	19, 20	syl 17	. . . . 5 |- ( ( et /\ th ) -> ch' )
22		simpl 473	. . . . 5 |- ( ( et /\ th ) -> et )
23	21, 22	jca 554	. . . 4 |- ( ( et /\ th ) -> ( ch' /\ et ) )
24	23	2eximi 1763	. . 3 |- ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) )
25		bnj248 30766	. . . . . . . 8 |- ( ( R FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R FrSe A /\ x e. A ) /\ ch' ) /\ et ) )
26		bnj605.31	. . . . . . . . . . 11 |- ( ch' <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
27		pm3.35 611	. . . . . . . . . . 11 |- ( ( ( R FrSe A /\ x e. A ) /\ ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) -> E! f ( f Fn m /\ ph' /\ ps' ) )
28	26, 27	sylan2b 492	. . . . . . . . . 10 |- ( ( ( R FrSe A /\ x e. A ) /\ ch' ) -> E! f ( f Fn m /\ ph' /\ ps' ) )
29		euex 2494	. . . . . . . . . 10 |- ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) )
30	28, 29	syl 17	. . . . . . . . 9 |- ( ( ( R FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) )
31		bnj605.17	. . . . . . . . 9 |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
32	30, 31	bnj1198 30866	. . . . . . . 8 |- ( ( ( R FrSe A /\ x e. A ) /\ ch' ) -> E. f ta )
33	25, 32	bnj832 30828	. . . . . . 7 |- ( ( R FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta )
34		bnj605.41	. . . . . . . . . . . . . 14 |- ( ( R FrSe A /\ ta /\ et ) -> f Fn n )
35		bnj605.42	. . . . . . . . . . . . . 14 |- ( ( R FrSe A /\ ta /\ et ) -> ph" )
36		bnj605.43	. . . . . . . . . . . . . 14 |- ( ( R FrSe A /\ ta /\ et ) -> ps" )
37	34, 35, 36	3jca 1242	. . . . . . . . . . . . 13 |- ( ( R FrSe A /\ ta /\ et ) -> ( f Fn n /\ ph" /\ ps" ) )
38	37	3com23 1271	. . . . . . . . . . . 12 |- ( ( R FrSe A /\ et /\ ta ) -> ( f Fn n /\ ph" /\ ps" ) )
39	38	3expia 1267	. . . . . . . . . . 11 |- ( ( R FrSe A /\ et ) -> ( ta -> ( f Fn n /\ ph" /\ ps" ) ) )
40	39	eximdv 1846	. . . . . . . . . 10 |- ( ( R FrSe A /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
41	40	adantlr 751	. . . . . . . . 9 |- ( ( ( R FrSe A /\ x e. A ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
42	41	adantlr 751	. . . . . . . 8 |- ( ( ( ( R FrSe A /\ x e. A ) /\ ch' ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
43	25, 42	sylbi 207	. . . . . . 7 |- ( ( R FrSe A /\ x e. A /\ ch' /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
44	33, 43	mpd 15	. . . . . 6 |- ( ( R FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( f Fn n /\ ph" /\ ps" ) )
45		bnj432 30782	. . . . . 6 |- ( ( R FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ch' /\ et ) /\ ( R FrSe A /\ x e. A ) ) )
46		biid 251	. . . . . . . 8 |- ( f Fn n <-> f Fn n )
47		bnj605.13	. . . . . . . . 9 |- ( ph" <-> [. f / f ]. ph )
48		sbcid 3452	. . . . . . . . 9 |- ( [. f / f ]. ph <-> ph )
49	47, 48	bitri 264	. . . . . . . 8 |- ( ph" <-> ph )
50		bnj605.14	. . . . . . . . 9 |- ( ps" <-> [. f / f ]. ps )
51		sbcid 3452	. . . . . . . . 9 |- ( [. f / f ]. ps <-> ps )
52	50, 51	bitri 264	. . . . . . . 8 |- ( ps" <-> ps )
53	46, 49, 52	3anbi123i 1251	. . . . . . 7 |- ( ( f Fn n /\ ph" /\ ps" ) <-> ( f Fn n /\ ph /\ ps ) )
54	53	exbii 1774	. . . . . 6 |- ( E. f ( f Fn n /\ ph" /\ ps" ) <-> E. f ( f Fn n /\ ph /\ ps ) )
55	44, 45, 54	3imtr3i 280	. . . . 5 |- ( ( ( ch' /\ et ) /\ ( R FrSe A /\ x e. A ) ) -> E. f ( f Fn n /\ ph /\ ps ) )
56	55	ex 450	. . . 4 |- ( ( ch' /\ et ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
57	56	exlimivv 1860	. . 3 |- ( E. m E. p ( ch' /\ et ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
58	11, 24, 57	3syl 18	. 2 |- ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
59	58	3impa 1259	1 |- ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   E!weu 2470   =/= wne 2794   A.wral 2912   _Vcvv 3200   [.wsbc 3435   (/)c0 3915   U_ciun 4520   class class class wbr 4653   _E cep 5028   suc csuc 5725   Fn wfn 5883   ` cfv 5888   omcom 7065   1oc1o 7553   /\ w-bnj17 30752   predc-bnj14 30754   FrSe w-bnj15 30758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-eprel 5029  df-suc 5729  df-bnj17 30753

This theorem is referenced by: (None)