Theorem ordiso2 7961

Description: Generalize ordiso 7962 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)

Assertion

Ref	Expression
ordiso2

Proof of Theorem ordiso2

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordsson 6625	. . . . . 6
2	1	3ad2ant2 1018	. . . . 5
3	2	sseld 3502	. . . 4
4		eleq1 2529	. . . . . . . 8
5		fveq2 5871	. . . . . . . . 9
6		id 22	. . . . . . . . 9
7	5, 6	eqeq12d 2479	. . . . . . . 8
8	4, 7	imbi12d 320	. . . . . . 7
9	8	imbi2d 316	. . . . . 6
10		r19.21v 2862	. . . . . . 7
11		ordelss 4899	. . . . . . . . . . . . . . . 16
12	11	3ad2antl2 1159	. . . . . . . . . . . . . . 15
13	12	sselda 3503	. . . . . . . . . . . . . 14
14		pm5.5 336	. . . . . . . . . . . . . 14
15	13, 14	syl 16	. . . . . . . . . . . . 13
16	15	ralbidva 2893	. . . . . . . . . . . 12
17		isof1o 6221	. . . . . . . . . . . . . . . . . . . 20
18	17	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 19
19	18	ad2antrr 725	. . . . . . . . . . . . . . . . . 18
20		simpll3 1037	. . . . . . . . . . . . . . . . . . 19
21		simpr 461	. . . . . . . . . . . . . . . . . . . 20
22		f1of 5821	. . . . . . . . . . . . . . . . . . . . . . . 24
23	17, 22	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . 22
25	24	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21
26		simplrl 761	. . . . . . . . . . . . . . . . . . . . 21
27		ffvelrn 6029	. . . . . . . . . . . . . . . . . . . . 21
28	25, 26, 27	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
29	21, 28	jca 532	. . . . . . . . . . . . . . . . . . 19
30		ordtr1 4926	. . . . . . . . . . . . . . . . . . 19
31	20, 29, 30	sylc 60	. . . . . . . . . . . . . . . . . 18
32		f1ocnvfv2 6183	. . . . . . . . . . . . . . . . . 18
33	19, 31, 32	syl2anc 661	. . . . . . . . . . . . . . . . 17
34	33, 21	eqeltrd 2545	. . . . . . . . . . . . . . . . . . 19
35		simpll1 1035	. . . . . . . . . . . . . . . . . . . . 21
36		f1ocnv 5833	. . . . . . . . . . . . . . . . . . . . . . 23
37		f1of 5821	. . . . . . . . . . . . . . . . . . . . . . 23
38	19, 36, 37	3syl 20	. . . . . . . . . . . . . . . . . . . . . 22
39		ffvelrn 6029	. . . . . . . . . . . . . . . . . . . . . 22
40	38, 31, 39	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
41		isorel 6222	. . . . . . . . . . . . . . . . . . . . 21
42	35, 40, 26, 41	syl12anc 1226	. . . . . . . . . . . . . . . . . . . 20
43		vex 3112	. . . . . . . . . . . . . . . . . . . . 21
44	43	epelc 4798	. . . . . . . . . . . . . . . . . . . 20
45		fvex 5881	. . . . . . . . . . . . . . . . . . . . 21
46	45	epelc 4798	. . . . . . . . . . . . . . . . . . . 20
47	42, 44, 46	3bitr3g 287	. . . . . . . . . . . . . . . . . . 19
48	34, 47	mpbird 232	. . . . . . . . . . . . . . . . . 18
49		simplrr 762	. . . . . . . . . . . . . . . . . 18
50		fveq2 5871	. . . . . . . . . . . . . . . . . . . 20
51		id 22	. . . . . . . . . . . . . . . . . . . 20
52	50, 51	eqeq12d 2479	. . . . . . . . . . . . . . . . . . 19
53	52	rspcv 3206	. . . . . . . . . . . . . . . . . 18
54	48, 49, 53	sylc 60	. . . . . . . . . . . . . . . . 17
55	33, 54	eqtr3d 2500	. . . . . . . . . . . . . . . 16
56	55, 48	eqeltrd 2545	. . . . . . . . . . . . . . 15
57		simprr 757	. . . . . . . . . . . . . . . . 17
58		fveq2 5871	. . . . . . . . . . . . . . . . . . 19
59		id 22	. . . . . . . . . . . . . . . . . . 19
60	58, 59	eqeq12d 2479	. . . . . . . . . . . . . . . . . 18
61	60	rspccva 3209	. . . . . . . . . . . . . . . . 17
62	57, 61	sylan 471	. . . . . . . . . . . . . . . 16
63		epel 4799	. . . . . . . . . . . . . . . . . . . 20
64	63	biimpri 206	. . . . . . . . . . . . . . . . . . 19
65	64	adantl 466	. . . . . . . . . . . . . . . . . 18
66		simpll1 1035	. . . . . . . . . . . . . . . . . . 19
67		simpl2 1000	. . . . . . . . . . . . . . . . . . . . 21
68		simprl 756	. . . . . . . . . . . . . . . . . . . . 21
69	67, 68, 11	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
70	69	sselda 3503	. . . . . . . . . . . . . . . . . . 19
71		simplrl 761	. . . . . . . . . . . . . . . . . . 19
72		isorel 6222	. . . . . . . . . . . . . . . . . . 19
73	66, 70, 71, 72	syl12anc 1226	. . . . . . . . . . . . . . . . . 18
74	65, 73	mpbid 210	. . . . . . . . . . . . . . . . 17
75	45	epelc 4798	. . . . . . . . . . . . . . . . 17
76	74, 75	sylib 196	. . . . . . . . . . . . . . . 16
77	62, 76	eqeltrrd 2546	. . . . . . . . . . . . . . 15
78	56, 77	impbida 832	. . . . . . . . . . . . . 14
79	78	eqrdv 2454	. . . . . . . . . . . . 13
80	79	expr 615	. . . . . . . . . . . 12
81	16, 80	sylbid 215	. . . . . . . . . . 11
82	81	ex 434	. . . . . . . . . 10
83	82	com23 78	. . . . . . . . 9
84	83	a2i 13	. . . . . . . 8
85	84	a1i 11	. . . . . . 7
86	10, 85	syl5bi 217	. . . . . 6
87	9, 86	tfis2 6691	. . . . 5
88	87	com3l 81	. . . 4
89	3, 88	mpdd 40	. . 3
90	89	ralrimiv 2869	. 2
91		fveq2 5871	. . . . . . . . 9
92		id 22	. . . . . . . . 9
93	91, 92	eqeq12d 2479	. . . . . . . 8
94	93	rspccva 3209	. . . . . . 7
95	94	adantll 713	. . . . . 6
96		ffvelrn 6029	. . . . . . . . 9
97	23, 96	sylan 471	. . . . . . . 8
98	97	3ad2antl1 1158	. . . . . . 7
99	98	adantlr 714	. . . . . 6
100	95, 99	eqeltrrd 2546	. . . . 5
101	100	ex 434	. . . 4
102		simpl1 999	. . . . . . . 8
103		f1ofo 5828	. . . . . . . . 9
104		forn 5803	. . . . . . . . 9
105	17, 103, 104	3syl 20	. . . . . . . 8
106	102, 105	syl 16	. . . . . . 7
107	106	eleq2d 2527	. . . . . 6
108		f1ofn 5822	. . . . . . . . . 10
109	17, 108	syl 16	. . . . . . . . 9
110	109	3ad2ant1 1017	. . . . . . . 8
111	110	adantr 465	. . . . . . 7
112		fvelrnb 5920	. . . . . . 7
113	111, 112	syl 16	. . . . . 6
114	107, 113	bitr3d 255	. . . . 5
115		fveq2 5871	. . . . . . . . . . . 12
116		id 22	. . . . . . . . . . . 12
117	115, 116	eqeq12d 2479	. . . . . . . . . . 11
118	117	rspcv 3206	. . . . . . . . . 10
119	118	a1i 11	. . . . . . . . 9
120		simpr 461	. . . . . . . . . . . . 13
121		simpl 457	. . . . . . . . . . . . 13
122	120, 121	eqtr3d 2500	. . . . . . . . . . . 12
123	122	adantl 466	. . . . . . . . . . 11
124		simplr 755	. . . . . . . . . . 11
125	123, 124	eqeltrd 2545	. . . . . . . . . 10
126	125	exp43 612	. . . . . . . . 9
127	119, 126	syldd 66	. . . . . . . 8
128	127	com23 78	. . . . . . 7
129	128	imp 429	. . . . . 6
130	129	rexlimdv 2947	. . . . 5
131	114, 130	sylbid 215	. . . 4
132	101, 131	impbid 191	. . 3
133	132	eqrdv 2454	. 2
134	90, 133	mpdan 668	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  C_wss 3475   class class class wbr 4452  cep 4794  Ordword 4882  con0 4883  `'ccnv 5003  rancrn 5005  Fnwfn 5588  -->wf 5589  -onto->wfo 5591  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594

This theorem is referenced by:  ordiso  7962  oieu  7985  oiid  7987

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-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  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-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602