Table of ContentsTable of Contents Mathbox for Frédéric Liné < Previous   Next >
Related theorems
Unicode version
Theorem injsurinj 14487
Description: If E is an injection and G a surjection (f |-> ((E o. f) o. G)) is an injection. Bourbaki E.II.31 prop. 2.
Hypothesis
Ref Expression
injsuinj.1 |- F1 = (f e. (B ^m A) |-> ((E o. f) o. G))
Assertion
Ref Expression
injsurinj |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1:(B ^m A)-1-1->(B1 ^m A1))
Distinct variable groups:   A,f   f,A1   B,f   f,B1   f,E   f,G
Proof of Theorem injsurinj
StepHypRef Expression
1 dff13 4850 . 2 |- (F1:(B ^m A)-1-1->(B1 ^m A1) <-> (F1:(B ^m A)-->(B1 ^m A1) /\ A.x e. (B ^m A)A.y e. (B ^m A)((F1` x) = (F1` y) -> x = y)))
2 injsuinj.1 . . . 4 |- F1 = (f e. (B ^m A) |-> ((E o. f) o. G))
32mapmapmap 14486 . . 3 |- ((E:B-->B1 /\ G:A1-->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1:(B ^m A)-->(B1 ^m A1))
4 f1f 4610 . . 3 |- (E:B-1-1->B1 -> E:B-->B1)
5 fof 4617 . . 3 |- (G:A1-onto->A -> G:A1-->A)
6 id 73 . . 3 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))
73, 4, 5, 6syl3an 1139 . 2 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1:(B ^m A)-->(B1 ^m A1))
8 simp1 876 . . . . . . . 8 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x e. (B ^m A))
9 coexg 4429 . . . . . . . . . . 11 |- ((E e. _V /\ x e. _V) -> (E o. x) e. _V)
104adantr 425 . . . . . . . . . . . . 13 |- ((E:B-1-1->B1 /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> E:B-->B1)
11 simprlr 457 . . . . . . . . . . . . 13 |- ((E:B-1-1->B1 /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> B e. _V)
12 fex 4595 . . . . . . . . . . . . 13 |- ((E:B-->B1 /\ B e. _V) -> E e. _V)
1310, 11, 12syl11anc 524 . . . . . . . . . . . 12 |- ((E:B-1-1->B1 /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> E e. _V)
14133adant2 895 . . . . . . . . . . 11 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> E e. _V)
15 visset 2295 . . . . . . . . . . 11 |- x e. _V
169, 14, 15sylancl 525 . . . . . . . . . 10 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (E o. x) e. _V)
1753ad2ant2 898 . . . . . . . . . . 11 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> G:A1-->A)
18 simp3rl 949 . . . . . . . . . . 11 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> A1 e. _V)
19 fex 4595 . . . . . . . . . . 11 |- ((G:A1-->A /\ A1 e. _V) -> G e. _V)
2017, 18, 19syl11anc 524 . . . . . . . . . 10 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> G e. _V)
21 coexg 4429 . . . . . . . . . 10 |- (((E o. x) e. _V /\ G e. _V) -> ((E o. x) o. G) e. _V)
2216, 20, 21syl11anc 524 . . . . . . . . 9 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> ((E o. x) o. G) e. _V)
23223ad2ant3 899 . . . . . . . 8 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((E o. x) o. G) e. _V)
248, 23jca 310 . . . . . . 7 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> (x e. (B ^m A) /\ ((E o. x) o. G) e. _V))
25 coeq2 4124 . . . . . . . . 9 |- (f = x -> (E o. f) = (E o. x))
2625coeq1d 4127 . . . . . . . 8 |- (f = x -> ((E o. f) o. G) = ((E o. x) o. G))
2726, 2fvmptg 5014 . . . . . . 7 |- ((x e. (B ^m A) /\ ((E o. x) o. G) e. _V) -> (F1` x) = ((E o. x) o. G))
28 simp2 877 . . . . . . . . . . 11 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> y e. (B ^m A))
29 coexg 4429 . . . . . . . . . . . . 13 |- ((E e. _V /\ y e. _V) -> (E o. y) e. _V)
30143ad2ant3 899 . . . . . . . . . . . . 13 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> E e. _V)
31 visset 2295 . . . . . . . . . . . . 13 |- y e. _V
3229, 30, 31sylancl 525 . . . . . . . . . . . 12 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> (E o. y) e. _V)
33203ad2ant3 899 . . . . . . . . . . . 12 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> G e. _V)
34 coexg 4429 . . . . . . . . . . . 12 |- (((E o. y) e. _V /\ G e. _V) -> ((E o. y) o. G) e. _V)
3532, 33, 34syl11anc 524 . . . . . . . . . . 11 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((E o. y) o. G) e. _V)
3628, 35jca 310 . . . . . . . . . 10 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> (y e. (B ^m A) /\ ((E o. y) o. G) e. _V))
37 coeq2 4124 . . . . . . . . . . . 12 |- (f = y -> (E o. f) = (E o. y))
3837coeq1d 4127 . . . . . . . . . . 11 |- (f = y -> ((E o. f) o. G) = ((E o. y) o. G))
3938, 2fvmptg 5014 . . . . . . . . . 10 |- ((y e. (B ^m A) /\ ((E o. y) o. G) e. _V) -> (F1` y) = ((E o. y) o. G))
40 eqtr 1904 . . . . . . . . . . . . . 14 |- ((((E o. x) o. G) = (F1` x) /\ (F1` x) = (F1` y)) -> ((E o. x) o. G) = (F1` y))
41 eqtr 1904 . . . . . . . . . . . . . . . 16 |- ((((E o. x) o. G) = (F1` y) /\ (F1` y) = ((E o. y) o. G)) -> ((E o. x) o. G) = ((E o. y) o. G))
42 simpr31 966 . . . . . . . . . . . . . . . . . . 19 |- ((((E o. x) o. G) = ((E o. y) o. G) /\ (x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))))) -> E:B-1-1->B1)
43 elmapg 5392 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. _V /\ A e. _V) -> (x e. (B ^m A) <-> x:A-->B))
4443ancoms 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. _V /\ B e. _V) -> (x e. (B ^m A) <-> x:A-->B))
4544biimpd 170 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. _V /\ B e. _V) -> (x e. (B ^m A) -> x:A-->B))
4645adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> (x e. (B ^m A) -> x:A-->B))
47463ad2ant3 899 . . . . . . . . . . . . . . . . . . . . . 22 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (x e. (B ^m A) -> x:A-->B))
4847impcom 378 . . . . . . . . . . . . . . . . . . . . 21 |- ((x e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x:A-->B)
49483adant2 895 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x:A-->B)
5049adantl 424 . . . . . . . . . . . . . . . . . . 19 |- ((((E o. x) o. G) = ((E o. y) o. G) /\ (x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))))) -> x:A-->B)
51 elmapg 5392 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. _V /\ A e. _V) -> (y e. (B ^m A) <-> y:A-->B))
5251ancoms 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. _V /\ B e. _V) -> (y e. (B ^m A) <-> y:A-->B))
5352biimpd 170 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. _V /\ B e. _V) -> (y e. (B ^m A) -> y:A-->B))
5453adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)) -> (y e. (B ^m A) -> y:A-->B))
55543ad2ant3 899 . . . . . . . . . . . . . . . . . . . . . 22 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> (y e. (B ^m A) -> y:A-->B))
5655impcom 378 . . . . . . . . . . . . . . . . . . . . 21 |- ((y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> y:A-->B)
57563adant1 894 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> y:A-->B)
5857adantl 424 . . . . . . . . . . . . . . . . . . 19 |- ((((E o. x) o. G) = ((E o. y) o. G) /\ (x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))))) -> y:A-->B)
5942, 50, 583jca 1050 . . . . . . . . . . . . . . . . . 18 |- ((((E o. x) o. G) = ((E o. y) o. G) /\ (x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))))) -> (E:B-1-1->B1 /\ x:A-->B /\ y:A-->B))
60 simp32 913 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> G:A1-onto->A)
6143ad2ant1 897 . . . . . . . . . . . . . . . . . . . . . 22 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> E:B-->B1)
62613ad2ant3 899 . . . . . . . . . . . . . . . . . . . . 21 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> E:B-->B1)
63 fco 4573 . . . . . . . . . . . . . . . . . . . . 21 |- ((E:B-->B1 /\ x:A-->B) -> (E o. x):A-->B1)
6462, 49, 63syl11anc 524 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> (E o. x):A-->B1)
65 fco 4573 . . . . . . . . . . . . . . . . . . . . 21 |- ((E:B-->B1 /\ y:A-->B) -> (E o. y):A-->B1)
6662, 57, 65syl11anc 524 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> (E o. y):A-->B1)
67 surrc2 14390 . . . . . . . . . . . . . . . . . . . . . 22 |- ((G:A1-onto->A /\ (E o. x) Fn A /\ (E o. y) Fn A) -> (((E o. x) o. G) = ((E o. y) o. G) <-> (E o. x) = (E o. y)))
68 id 73 . . . . . . . . . . . . . . . . . . . . . 22 |- (G:A1-onto->A -> G:A1-onto->A)
69 ffn 4562 . . . . . . . . . . . . . . . . . . . . . 22 |- ((E o. x):A-->B1 -> (E o. x) Fn A)
70 ffn 4562 . . . . . . . . . . . . . . . . . . . . . 22 |- ((E o. y):A-->B1 -> (E o. y) Fn A)
7167, 68, 69, 70syl3an 1139 . . . . . . . . . . . . . . . . . . . . 21 |- ((G:A1-onto->A /\ (E o. x):A-->B1 /\ (E o. y):A-->B1) -> (((E o. x) o. G) = ((E o. y) o. G) <-> (E o. x) = (E o. y)))
7271biimpd 170 . . . . . . . . . . . . . . . . . . . 20 |- ((G:A1-onto->A /\ (E o. x):A-->B1 /\ (E o. y):A-->B1) -> (((E o. x) o. G) = ((E o. y) o. G) -> (E o. x) = (E o. y)))
7360, 64, 66, 72syl111anc 1100 . . . . . . . . . . . . . . . . . . 19 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> (((E o. x) o. G) = ((E o. y) o. G) -> (E o. x) = (E o. y)))
7473impcom 378 . . . . . . . . . . . . . . . . . 18 |- ((((E o. x) o. G) = ((E o. y) o. G) /\ (x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))))) -> (E o. x) = (E o. y))
75 njtlc 14389 . . . . . . . . . . . . . . . . . 18 |- ((E:B-1-1->B1 /\ x:A-->B /\ y:A-->B) -> ((E o. x) = (E o. y) -> x = y))
7659, 74, 75sylc 83 . . . . . . . . . . . . . . . . 17 |- ((((E o. x) o. G) = ((E o. y) o. G) /\ (x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))))) -> x = y)
7776ex 402 . . . . . . . . . . . . . . . 16 |- (((E o. x) o. G) = ((E o. y) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x = y))
7841, 77syl 12 . . . . . . . . . . . . . . 15 |- ((((E o. x) o. G) = (F1` y) /\ (F1` y) = ((E o. y) o. G)) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x = y))
7978ex 402 . . . . . . . . . . . . . 14 |- (((E o. x) o. G) = (F1` y) -> ((F1` y) = ((E o. y) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x = y)))
8040, 79syl 12 . . . . . . . . . . . . 13 |- ((((E o. x) o. G) = (F1` x) /\ (F1` x) = (F1` y)) -> ((F1` y) = ((E o. y) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x = y)))
8180ex 402 . . . . . . . . . . . 12 |- (((E o. x) o. G) = (F1` x) -> ((F1` x) = (F1` y) -> ((F1` y) = ((E o. y) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x = y))))
8281eqcoms 1887 . . . . . . . . . . 11 |- ((F1` x) = ((E o. x) o. G) -> ((F1` x) = (F1` y) -> ((F1` y) = ((E o. y) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> x = y))))
8382com4t 44 . . . . . . . . . 10 |- ((F1` y) = ((E o. y) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((F1` x) = ((E o. x) o. G) -> ((F1` x) = (F1` y) -> x = y))))
8436, 39, 833syl 24 . . . . . . . . 9 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((F1` x) = ((E o. x) o. G) -> ((F1` x) = (F1` y) -> x = y))))
8584pm2.43i 78 . . . . . . . 8 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((F1` x) = ((E o. x) o. G) -> ((F1` x) = (F1` y) -> x = y)))
8685com12 14 . . . . . . 7 |- ((F1` x) = ((E o. x) o. G) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((F1` x) = (F1` y) -> x = y)))
8724, 27, 863syl 24 . . . . . 6 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((F1` x) = (F1` y) -> x = y)))
8887pm2.43i 78 . . . . 5 |- ((x e. (B ^m A) /\ y e. (B ^m A) /\ (E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V)))) -> ((F1` x) = (F1` y) -> x = y))
89883expia 1069 . . . 4 |- ((x e. (B ^m A) /\ y e. (B ^m A)) -> ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> ((F1` x) = (F1` y) -> x = y)))
9089com12 14 . . 3 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> ((x e. (B ^m A) /\ y e. (B ^m A)) -> ((F1` x) = (F1` y) -> x = y)))
9190r19.21aivv 2183 . 2 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> A.x e. (B ^m A)A.y e. (B ^m A)((F1` x) = (F1` y) -> x = y))
921, 7, 91sylanbrc 527 1 |- ((E:B-1-1->B1 /\ G:A1-onto->A /\ ((A e. _V /\ B e. _V) /\ (A1 e. _V /\ B1 e. _V))) -> F1:(B ^m A)-1-1->(B1 ^m A1))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   o. ccom 3990   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884   e. cmpt 5004   ^m cmap 5381
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-map 5383
Copyright terms: Public domain