Metamath Proof Explorer

Theorem isomin

Description: Isomorphisms preserve minimal elements. Note that (`' R " { D } ) ` is Takeuti and Zaring's idiom for the initial segment { x | x R D } . Proposition 6.31(1) of TakeutiZaring p. 33. (Contributed by NM, 19-Apr-2004)

Ref Expression
Assertion isomin 
|- ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( C i^i ( `' R " { D } ) ) = (/) <-> ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 neq0 
 |-  ( -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) <-> E. y y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) )
2 vex 
 |-  y e. _V
3 2 elima 
 |-  ( y e. ( H " C ) <-> E. x e. C x H y )
4 ssel 
 |-  ( C C_ A -> ( x e. C -> x e. A ) )
5 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
6 f1ofn 
 |-  ( H : A -1-1-onto-> B -> H Fn A )
7 fnbrfvb 
 |-  ( ( H Fn A /\ x e. A ) -> ( ( H ` x ) = y <-> x H y ) )
8 7 ex 
 |-  ( H Fn A -> ( x e. A -> ( ( H ` x ) = y <-> x H y ) ) )
9 5 6 8 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( x e. A -> ( ( H ` x ) = y <-> x H y ) ) )
10 4 9 syl9r 
 |-  ( H Isom R , S ( A , B ) -> ( C C_ A -> ( x e. C -> ( ( H ` x ) = y <-> x H y ) ) ) )
11 10 imp31 
 |-  ( ( ( H Isom R , S ( A , B ) /\ C C_ A ) /\ x e. C ) -> ( ( H ` x ) = y <-> x H y ) )
12 11 rexbidva 
 |-  ( ( H Isom R , S ( A , B ) /\ C C_ A ) -> ( E. x e. C ( H ` x ) = y <-> E. x e. C x H y ) )
13 3 12 bitr4id 
 |-  ( ( H Isom R , S ( A , B ) /\ C C_ A ) -> ( y e. ( H " C ) <-> E. x e. C ( H ` x ) = y ) )
14 fvex 
 |-  ( H ` D ) e. _V
15 2 eliniseg 
 |-  ( ( H ` D ) e. _V -> ( y e. ( `' S " { ( H ` D ) } ) <-> y S ( H ` D ) ) )
16 14 15 mp1i 
 |-  ( ( H Isom R , S ( A , B ) /\ C C_ A ) -> ( y e. ( `' S " { ( H ` D ) } ) <-> y S ( H ` D ) ) )
17 13 16 anbi12d 
 |-  ( ( H Isom R , S ( A , B ) /\ C C_ A ) -> ( ( y e. ( H " C ) /\ y e. ( `' S " { ( H ` D ) } ) ) <-> ( E. x e. C ( H ` x ) = y /\ y S ( H ` D ) ) ) )
18 elin 
 |-  ( y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) <-> ( y e. ( H " C ) /\ y e. ( `' S " { ( H ` D ) } ) ) )
19 r19.41v 
 |-  ( E. x e. C ( ( H ` x ) = y /\ y S ( H ` D ) ) <-> ( E. x e. C ( H ` x ) = y /\ y S ( H ` D ) ) )
20 17 18 19 3bitr4g 
 |-  ( ( H Isom R , S ( A , B ) /\ C C_ A ) -> ( y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) <-> E. x e. C ( ( H ` x ) = y /\ y S ( H ` D ) ) ) )
21 20 adantrr 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) <-> E. x e. C ( ( H ` x ) = y /\ y S ( H ` D ) ) ) )
22 breq1 
 |-  ( ( H ` x ) = y -> ( ( H ` x ) S ( H ` D ) <-> y S ( H ` D ) ) )
23 22 biimpar 
 |-  ( ( ( H ` x ) = y /\ y S ( H ` D ) ) -> ( H ` x ) S ( H ` D ) )
24 vex 
 |-  x e. _V
25 24 eliniseg 
 |-  ( D e. A -> ( x e. ( `' R " { D } ) <-> x R D ) )
26 25 ad2antll 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) <-> x R D ) )
27 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D <-> ( H ` x ) S ( H ` D ) ) )
28 26 27 bitrd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) <-> ( H ` x ) S ( H ` D ) ) )
29 23 28 syl5ibr 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( ( ( H ` x ) = y /\ y S ( H ` D ) ) -> x e. ( `' R " { D } ) ) )
30 29 exp32 
 |-  ( H Isom R , S ( A , B ) -> ( x e. A -> ( D e. A -> ( ( ( H ` x ) = y /\ y S ( H ` D ) ) -> x e. ( `' R " { D } ) ) ) ) )
31 4 30 syl9r 
 |-  ( H Isom R , S ( A , B ) -> ( C C_ A -> ( x e. C -> ( D e. A -> ( ( ( H ` x ) = y /\ y S ( H ` D ) ) -> x e. ( `' R " { D } ) ) ) ) ) )
32 31 com34 
 |-  ( H Isom R , S ( A , B ) -> ( C C_ A -> ( D e. A -> ( x e. C -> ( ( ( H ` x ) = y /\ y S ( H ` D ) ) -> x e. ( `' R " { D } ) ) ) ) ) )
33 32 imp32 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( ( ( H ` x ) = y /\ y S ( H ` D ) ) -> x e. ( `' R " { D } ) ) ) )
34 33 reximdvai 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( E. x e. C ( ( H ` x ) = y /\ y S ( H ` D ) ) -> E. x e. C x e. ( `' R " { D } ) ) )
35 21 34 sylbid 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) -> E. x e. C x e. ( `' R " { D } ) ) )
36 elin 
 |-  ( x e. ( C i^i ( `' R " { D } ) ) <-> ( x e. C /\ x e. ( `' R " { D } ) ) )
37 36 exbii 
 |-  ( E. x x e. ( C i^i ( `' R " { D } ) ) <-> E. x ( x e. C /\ x e. ( `' R " { D } ) ) )
38 neq0 
 |-  ( -. ( C i^i ( `' R " { D } ) ) = (/) <-> E. x x e. ( C i^i ( `' R " { D } ) ) )
39 df-rex 
 |-  ( E. x e. C x e. ( `' R " { D } ) <-> E. x ( x e. C /\ x e. ( `' R " { D } ) ) )
40 37 38 39 3bitr4i 
 |-  ( -. ( C i^i ( `' R " { D } ) ) = (/) <-> E. x e. C x e. ( `' R " { D } ) )
41 35 40 syl6ibr 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) -> -. ( C i^i ( `' R " { D } ) ) = (/) ) )
42 41 exlimdv 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( E. y y e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) -> -. ( C i^i ( `' R " { D } ) ) = (/) ) )
43 1 42 syl5bi 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) -> -. ( C i^i ( `' R " { D } ) ) = (/) ) )
44 43 con4d 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( C i^i ( `' R " { D } ) ) = (/) -> ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )
45 5 6 syl 
 |-  ( H Isom R , S ( A , B ) -> H Fn A )
46 fnfvima 
 |-  ( ( H Fn A /\ C C_ A /\ x e. C ) -> ( H ` x ) e. ( H " C ) )
47 46 3expia 
 |-  ( ( H Fn A /\ C C_ A ) -> ( x e. C -> ( H ` x ) e. ( H " C ) ) )
48 47 adantrr 
 |-  ( ( H Fn A /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( H ` x ) e. ( H " C ) ) )
49 45 48 sylan 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( H ` x ) e. ( H " C ) ) )
50 49 adantrd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( H ` x ) e. ( H " C ) ) )
51 27 biimpd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D -> ( H ` x ) S ( H ` D ) ) )
52 fvex 
 |-  ( H ` x ) e. _V
53 52 eliniseg 
 |-  ( ( H ` D ) e. _V -> ( ( H ` x ) e. ( `' S " { ( H ` D ) } ) <-> ( H ` x ) S ( H ` D ) ) )
54 14 53 ax-mp 
 |-  ( ( H ` x ) e. ( `' S " { ( H ` D ) } ) <-> ( H ` x ) S ( H ` D ) )
55 51 54 syl6ibr 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) )
56 26 55 sylbid 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) )
57 56 exp32 
 |-  ( H Isom R , S ( A , B ) -> ( x e. A -> ( D e. A -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) )
58 4 57 syl9r 
 |-  ( H Isom R , S ( A , B ) -> ( C C_ A -> ( x e. C -> ( D e. A -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) )
59 58 com34 
 |-  ( H Isom R , S ( A , B ) -> ( C C_ A -> ( D e. A -> ( x e. C -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) ) ) )
60 59 imp32 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. C -> ( x e. ( `' R " { D } ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) )
61 60 impd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) )
62 50 61 jcad 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( x e. C /\ x e. ( `' R " { D } ) ) -> ( ( H ` x ) e. ( H " C ) /\ ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) ) )
63 elin 
 |-  ( ( H ` x ) e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) <-> ( ( H ` x ) e. ( H " C ) /\ ( H ` x ) e. ( `' S " { ( H ` D ) } ) ) )
64 62 36 63 3imtr4g 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. ( C i^i ( `' R " { D } ) ) -> ( H ` x ) e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) ) )
65 n0i 
 |-  ( ( H ` x ) e. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) )
66 64 65 syl6 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( x e. ( C i^i ( `' R " { D } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )
67 66 exlimdv 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( E. x x e. ( C i^i ( `' R " { D } ) ) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )
68 38 67 syl5bi 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( -. ( C i^i ( `' R " { D } ) ) = (/) -> -. ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )
69 44 68 impcon4bid 
 |-  ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( C i^i ( `' R " { D } ) ) = (/) <-> ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )