This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem propssopi

Description: If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 16-Jun-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a 
|- A e. _V
snopeqop.b 
|- B e. _V
propeqop.c 
|- C e. _V
propeqop.d 
|- D e. _V
propeqop.e 
|- E e. _V
propeqop.f 
|- F e. _V
Assertion propssopi 
|- ( { <. A , B >. , <. C , D >. } C_ <. E , F >. -> A = C )

Proof

Step Hyp Ref Expression
1 snopeqop.a 
 |-  A e. _V
2 snopeqop.b 
 |-  B e. _V
3 propeqop.c 
 |-  C e. _V
4 propeqop.d 
 |-  D e. _V
5 propeqop.e 
 |-  E e. _V
6 propeqop.f 
 |-  F e. _V
7 5 6 dfop 
 |-  <. E , F >. = { { E } , { E , F } }
8 7 sseq2i 
 |-  ( { <. A , B >. , <. C , D >. } C_ <. E , F >. <-> { <. A , B >. , <. C , D >. } C_ { { E } , { E , F } } )
9 sspr 
 |-  ( { <. A , B >. , <. C , D >. } C_ { { E } , { E , F } } <-> ( ( { <. A , B >. , <. C , D >. } = (/) \/ { <. A , B >. , <. C , D >. } = { { E } } ) \/ ( { <. A , B >. , <. C , D >. } = { { E , F } } \/ { <. A , B >. , <. C , D >. } = { { E } , { E , F } } ) ) )
10 opex 
 |-  <. A , B >. e. _V
11 10 prnz 
 |-  { <. A , B >. , <. C , D >. } =/= (/)
12 eqneqall 
 |-  ( { <. A , B >. , <. C , D >. } = (/) -> ( { <. A , B >. , <. C , D >. } =/= (/) -> A = C ) )
13 11 12 mpi 
 |-  ( { <. A , B >. , <. C , D >. } = (/) -> A = C )
14 opex 
 |-  <. C , D >. e. _V
15 10 14 preqsn 
 |-  ( { <. A , B >. , <. C , D >. } = { { E } } <-> ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E } ) )
16 1 2 opth 
 |-  ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )
17 simpl 
 |-  ( ( A = C /\ B = D ) -> A = C )
18 16 17 sylbi 
 |-  ( <. A , B >. = <. C , D >. -> A = C )
19 18 adantr 
 |-  ( ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E } ) -> A = C )
20 15 19 sylbi 
 |-  ( { <. A , B >. , <. C , D >. } = { { E } } -> A = C )
21 13 20 jaoi 
 |-  ( ( { <. A , B >. , <. C , D >. } = (/) \/ { <. A , B >. , <. C , D >. } = { { E } } ) -> A = C )
22 10 14 preqsn 
 |-  ( { <. A , B >. , <. C , D >. } = { { E , F } } <-> ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E , F } ) )
23 17 a1d 
 |-  ( ( A = C /\ B = D ) -> ( <. C , D >. = { E , F } -> A = C ) )
24 16 23 sylbi 
 |-  ( <. A , B >. = <. C , D >. -> ( <. C , D >. = { E , F } -> A = C ) )
25 24 imp 
 |-  ( ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E , F } ) -> A = C )
26 22 25 sylbi 
 |-  ( { <. A , B >. , <. C , D >. } = { { E , F } } -> A = C )
27 7 eqcomi 
 |-  { { E } , { E , F } } = <. E , F >.
28 27 eqeq2i 
 |-  ( { <. A , B >. , <. C , D >. } = { { E } , { E , F } } <-> { <. A , B >. , <. C , D >. } = <. E , F >. )
29 1 2 3 4 5 6 propeqop 
 |-  ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
30 28 29 bitri 
 |-  ( { <. A , B >. , <. C , D >. } = { { E } , { E , F } } <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
31 simpll 
 |-  ( ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) -> A = C )
32 30 31 sylbi 
 |-  ( { <. A , B >. , <. C , D >. } = { { E } , { E , F } } -> A = C )
33 26 32 jaoi 
 |-  ( ( { <. A , B >. , <. C , D >. } = { { E , F } } \/ { <. A , B >. , <. C , D >. } = { { E } , { E , F } } ) -> A = C )
34 21 33 jaoi 
 |-  ( ( ( { <. A , B >. , <. C , D >. } = (/) \/ { <. A , B >. , <. C , D >. } = { { E } } ) \/ ( { <. A , B >. , <. C , D >. } = { { E , F } } \/ { <. A , B >. , <. C , D >. } = { { E } , { E , F } } ) ) -> A = C )
35 9 34 sylbi 
 |-  ( { <. A , B >. , <. C , D >. } C_ { { E } , { E , F } } -> A = C )
36 8 35 sylbi 
 |-  ( { <. A , B >. , <. C , D >. } C_ <. E , F >. -> A = C )