Metamath Proof Explorer


Theorem isfin6

Description: Definition of a VI-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

Ref Expression
Assertion isfin6 AFinVIA2𝑜AA×A

Proof

Step Hyp Ref Expression
1 df-fin6 FinVI=x|x2𝑜xx×x
2 1 eleq2i AFinVIAx|x2𝑜xx×x
3 relsdom Rel
4 3 brrelex1i A2𝑜AV
5 3 brrelex1i AA×AAV
6 4 5 jaoi A2𝑜AA×AAV
7 breq1 x=Ax2𝑜A2𝑜
8 id x=Ax=A
9 8 sqxpeqd x=Ax×x=A×A
10 8 9 breq12d x=Axx×xAA×A
11 7 10 orbi12d x=Ax2𝑜xx×xA2𝑜AA×A
12 6 11 elab3 Ax|x2𝑜xx×xA2𝑜AA×A
13 2 12 bitri AFinVIA2𝑜AA×A