Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mat1dimbas Structured version   Unicode version

Theorem mat1dimbas 31057
 Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019.)
Hypotheses
Ref Expression
mat1dim.a Mat
mat1dim.b
mat1dim.o
Assertion
Ref Expression
mat1dimbas

Proof of Theorem mat1dimbas
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 risset 2885 . . . . . 6
21biimpi 194 . . . . 5
3 eqcom 2463 . . . . . 6
43rexbii 2862 . . . . 5
52, 4sylibr 212 . . . 4
7 mat1dim.o . . . . . . 7
8 opex 4667 . . . . . . 7
97, 8eqeltri 2538 . . . . . 6
10 simp3 990 . . . . . 6
11 opthg 4678 . . . . . 6
129, 10, 11sylancr 663 . . . . 5
13 opex 4667 . . . . . 6
14 sneqbg 4154 . . . . . 6
1513, 14ax-mp 5 . . . . 5
16 eqid 2454 . . . . . 6
1716biantrur 506 . . . . 5
1812, 15, 173bitr4g 288 . . . 4
1918rexbidv 2868 . . 3
206, 19mpbird 232 . 2
21 mat1dim.a . . . 4 Mat
22 mat1dim.b . . . 4
2321, 22, 7mat1dimelbas 31056 . . 3