Theorem f1owe 3981

Description: Well-ordering of isomorphic relations.

Hypothesis

Ref	Expression
f1owe.1	|- R = {<.x, y>. | (F` x)S(F` y)}

Assertion

Ref	Expression
f1owe	|- (F:A-1-1-onto->B -> (S We B -> R We A))

Distinct variable groups:   x,y,S   x,F,y

Proof of Theorem f1owe

Step	Hyp	Ref	Expression
1		fveq2 3800	. . . . . 6 |- (x = z -> (F` x) = (F` z))
2	1	breq1d 2679	. . . . 5 |- (x = z -> ((F` x)S(F` y) <-> (F` z)S(F` y)))
3		fveq2 3800	. . . . . 6 |- (y = w -> (F` y) = (F` w))
4	3	breq2d 2680	. . . . 5 |- (y = w -> ((F` z)S(F` y) <-> (F` z)S(F` w)))
5		f1owe.1	. . . . 5 |- R = {<.x, y>. | (F` x)S(F` y)}
6	2, 4, 5	brabg 2871	. . . 4 |- ((z e. A /\ w e. A) -> (zRw <-> (F` z)S(F` w)))
7	6	rgen2a 1737	. . 3 |- A.z e. A A.w e. A (zRw <-> (F` z)S(F` w))
8		df-iso 3254	. . . 4 |- (F Isom R, S (A, B) <-> (F:A-1-1-onto->B /\ A.z e. A A.w e. A (zRw <-> (F` z)S(F` w))))
9		isowe 3979	. . . 4 |- (F Isom R, S (A, B) -> (R We A <-> S We B))
10	8, 9	sylbir 199	. . 3 |- ((F:A-1-1-onto->B /\ A.z e. A A.w e. A (zRw <-> (F` z)S(F` w))) -> (R We A <-> S We B))
11	7, 10	mpan2 699	. 2 |- (F:A-1-1-onto->B -> (R We A <-> S We B))
12	11	biimprd 152	1 |- (F:A-1-1-onto->B -> (S We B -> R We A))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 988  A.wral 1683   class class class wbr 2669  {copab 2717   We wwe 2971  -1-1-onto->wf1o 3236  ` cfv 3237   Isom wiso 3238

This theorem is referenced by:  weth 4873

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-rep 2744  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-tp 2460  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-po 2894  df-so 2904  df-fr 2972  df-we 2989  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-f1 3250  df-fo 3251  df-f1o 3252  df-fv 3253  df-iso 3254

Copyright terms: Public domain