Metamath Proof Explorer

Theorem cnvf1olem

Description: Lemma for cnvf1o . (Contributed by Mario Carneiro, 27-Apr-2014)

Ref Expression
Assertion cnvf1olem 
|- ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> ( C e. `' A /\ B = U. `' { C } ) )

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> C = U. `' { B } )
2 1st2nd 
 |-  ( ( Rel A /\ B e. A ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
3 2 adantrr 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
4 3 sneqd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> { B } = { <. ( 1st ` B ) , ( 2nd ` B ) >. } )
5 4 cnveqd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> `' { B } = `' { <. ( 1st ` B ) , ( 2nd ` B ) >. } )
6 5 unieqd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> U. `' { B } = U. `' { <. ( 1st ` B ) , ( 2nd ` B ) >. } )
7 1 6 eqtrd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> C = U. `' { <. ( 1st ` B ) , ( 2nd ` B ) >. } )
8 opswap 
 |-  U. `' { <. ( 1st ` B ) , ( 2nd ` B ) >. } = <. ( 2nd ` B ) , ( 1st ` B ) >.
9 7 8 eqtrdi 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> C = <. ( 2nd ` B ) , ( 1st ` B ) >. )
10 simprl 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> B e. A )
11 3 10 eqeltrrd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> <. ( 1st ` B ) , ( 2nd ` B ) >. e. A )
12 fvex 
 |-  ( 2nd ` B ) e. _V
13 fvex 
 |-  ( 1st ` B ) e. _V
14 12 13 opelcnv 
 |-  ( <. ( 2nd ` B ) , ( 1st ` B ) >. e. `' A <-> <. ( 1st ` B ) , ( 2nd ` B ) >. e. A )
15 11 14 sylibr 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> <. ( 2nd ` B ) , ( 1st ` B ) >. e. `' A )
16 9 15 eqeltrd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> C e. `' A )
17 opswap 
 |-  U. `' { <. ( 2nd ` B ) , ( 1st ` B ) >. } = <. ( 1st ` B ) , ( 2nd ` B ) >.
18 17 eqcomi 
 |-  <. ( 1st ` B ) , ( 2nd ` B ) >. = U. `' { <. ( 2nd ` B ) , ( 1st ` B ) >. }
19 9 sneqd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> { C } = { <. ( 2nd ` B ) , ( 1st ` B ) >. } )
20 19 cnveqd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> `' { C } = `' { <. ( 2nd ` B ) , ( 1st ` B ) >. } )
21 20 unieqd 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> U. `' { C } = U. `' { <. ( 2nd ` B ) , ( 1st ` B ) >. } )
22 18 3 21 3eqtr4a 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> B = U. `' { C } )
23 16 22 jca 
 |-  ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> ( C e. `' A /\ B = U. `' { C } ) )