Theorem wemaplem2 7993

Description: Lemma for wemapso 7997. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.)

Hypotheses

Ref	Expression
wemapso.t
wemaplem2.a
wemaplem2.p
wemaplem2.x
wemaplem2.q
wemaplem2.r
wemaplem2.s
wemaplem2.px1
wemaplem2.px2
wemaplem2.px3
wemaplem2.xq1
wemaplem2.xq2
wemaplem2.xq3

Assertion

Ref	Expression
wemaplem2

Distinct variable groups:   ,,,,   ,,,   ,,,,,,,   ,,,,,,,   P,,,,,,,   Q,,,,,,,   ,,,,,,,   S,,,,,,,

Proof of Theorem wemaplem2

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wemaplem2.px1	. . . 4
2		wemaplem2.xq1	. . . 4
3	1, 2	ifcld 3984	. . 3
4		wemaplem2.px2	. . . . . . 7
5	4	adantr 465	. . . . . 6
6		wemaplem2.xq3	. . . . . . . 8
7		breq1 4455	. . . . . . . . . 10
8		fveq2 5871	. . . . . . . . . . 11
9		fveq2 5871	. . . . . . . . . . 11
10	8, 9	eqeq12d 2479	. . . . . . . . . 10
11	7, 10	imbi12d 320	. . . . . . . . 9
12	11	rspcva 3208	. . . . . . . 8
13	1, 6, 12	syl2anc 661	. . . . . . 7
14	13	imp 429	. . . . . 6
15	5, 14	breqtrd 4476	. . . . 5
16		iftrue 3947	. . . . . . . 8
17	16	fveq2d 5875	. . . . . . 7
18	16	fveq2d 5875	. . . . . . 7
19	17, 18	breq12d 4465	. . . . . 6
20	19	adantl 466	. . . . 5
21	15, 20	mpbird 232	. . . 4
22		wemaplem2.s	. . . . . . 7
23	22	adantr 465	. . . . . 6
24		wemaplem2.p	. . . . . . . . . 10
25		elmapi 7460	. . . . . . . . . 10
26	24, 25	syl 16	. . . . . . . . 9
27	26, 2	ffvelrnd 6032	. . . . . . . 8
28		wemaplem2.x	. . . . . . . . . 10
29		elmapi 7460	. . . . . . . . . 10
30	28, 29	syl 16	. . . . . . . . 9
31	30, 2	ffvelrnd 6032	. . . . . . . 8
32		wemaplem2.q	. . . . . . . . . 10
33		elmapi 7460	. . . . . . . . . 10
34	32, 33	syl 16	. . . . . . . . 9
35	34, 2	ffvelrnd 6032	. . . . . . . 8
36	27, 31, 35	3jca 1176	. . . . . . 7
37	36	adantr 465	. . . . . 6
38		fveq2 5871	. . . . . . . . 9
39		fveq2 5871	. . . . . . . . 9
40	38, 39	breq12d 4465	. . . . . . . 8
41	4, 40	syl5ibcom 220	. . . . . . 7
42	41	imp 429	. . . . . 6
43		wemaplem2.xq2	. . . . . . 7
44	43	adantr 465	. . . . . 6
45		potr 4817	. . . . . . 7
46	45	imp 429	. . . . . 6
47	23, 37, 42, 44, 46	syl22anc 1229	. . . . 5
48		ifeq1 3945	. . . . . . . . 9
49		ifid 3978	. . . . . . . . 9
50	48, 49	syl6eq 2514	. . . . . . . 8
51	50	fveq2d 5875	. . . . . . 7
52	50	fveq2d 5875	. . . . . . 7
53	51, 52	breq12d 4465	. . . . . 6
54	53	adantl 466	. . . . 5
55	47, 54	mpbird 232	. . . 4
56		wemaplem2.px3	. . . . . . . 8
57		breq1 4455	. . . . . . . . . 10
58		fveq2 5871	. . . . . . . . . . 11
59		fveq2 5871	. . . . . . . . . . 11
60	58, 59	eqeq12d 2479	. . . . . . . . . 10
61	57, 60	imbi12d 320	. . . . . . . . 9
62	61	rspcva 3208	. . . . . . . 8
63	2, 56, 62	syl2anc 661	. . . . . . 7
64	63	imp 429	. . . . . 6
65	43	adantr 465	. . . . . 6
66	64, 65	eqbrtrd 4472	. . . . 5
67		wemaplem2.r	. . . . . . . . 9
68		sopo 4822	. . . . . . . . 9
69	67, 68	syl 16	. . . . . . . 8
70		po2nr 4818	. . . . . . . 8
71	69, 2, 1, 70	syl12anc 1226	. . . . . . 7
72		nan 580	. . . . . . 7
73	71, 72	mpbi 208	. . . . . 6
74		iffalse 3950	. . . . . . . 8
75	74	fveq2d 5875	. . . . . . 7
76	74	fveq2d 5875	. . . . . . 7
77	75, 76	breq12d 4465	. . . . . 6
78	73, 77	syl 16	. . . . 5
79	66, 78	mpbird 232	. . . 4
80		solin 4828	. . . . 5
81	67, 1, 2, 80	syl12anc 1226	. . . 4
82	21, 55, 79, 81	mpjao3dan 1295	. . 3
83		r19.26 2984	. . . . 5
84	56, 6, 83	sylanbrc 664	. . . 4
85	67, 1, 2	3jca 1176	. . . . 5
86		prth 571	. . . . . . 7
87		eqtr 2483	. . . . . . 7
88	86, 87	syl6 33	. . . . . 6
89	88	ralimi 2850	. . . . 5
90		simpl1 999	. . . . . . . . 9
91		simpr 461	. . . . . . . . 9
92		simpl2 1000	. . . . . . . . 9
93		simpl3 1001	. . . . . . . . 9
94		soltmin 5411	. . . . . . . . 9
95	90, 91, 92, 93, 94	syl13anc 1230	. . . . . . . 8
96	95	biimpd 207	. . . . . . 7
97	96	imim1d 75	. . . . . 6
98	97	ralimdva 2865	. . . . 5
99	85, 89, 98	syl2im 38	. . . 4
100	84, 99	mpd 15	. . 3
101		fveq2 5871	. . . . . 6
102		fveq2 5871	. . . . . 6
103	101, 102	breq12d 4465	. . . . 5
104		breq2 4456	. . . . . . 7
105	104	imbi1d 317	. . . . . 6
106	105	ralbidv 2896	. . . . 5
107	103, 106	anbi12d 710	. . . 4
108	107	rspcev 3210	. . 3
109	3, 82, 100, 108	syl12anc 1226	. 2
110		wemapso.t	. . . 4
111	110	wemaplem1 7992	. . 3
112	24, 32, 111	syl2anc 661	. 2
113	109, 112	mpbird 232	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  \/w3o 972  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  cvv 3109  ifcif 3941   class class class wbr 4452  {copab 4509  Powpo 4803  Orwor 4804  -->wf 5589  `cfv 5593  (class class class)co 6296  cmap 7439

This theorem is referenced by:  wemaplem3  7994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6800  df-2nd 6801  df-map 7441