Metamath Proof Explorer

Theorem opfi1uzind

Description: Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses opfi1uzind.e 
|- E e. _V
opfi1uzind.f 
|- F e. _V
opfi1uzind.l 
|- L e. NN0
opfi1uzind.1 
|- ( ( v = V /\ e = E ) -> ( ps <-> ph ) )
opfi1uzind.2 
|- ( ( v = w /\ e = f ) -> ( ps <-> th ) )
opfi1uzind.3 
|- ( ( <. v , e >. e. G /\ n e. v ) -> <. ( v \ { n } ) , F >. e. G )
opfi1uzind.4 
|- ( ( w = ( v \ { n } ) /\ f = F ) -> ( th <-> ch ) )
opfi1uzind.base 
|- ( ( <. v , e >. e. G /\ ( # ` v ) = L ) -> ps )
opfi1uzind.step 
|- ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
Assertion opfi1uzind 
|- ( ( <. V , E >. e. G /\ V e. Fin /\ L <_ ( # ` V ) ) -> ph )

Proof

Step Hyp Ref Expression
1 opfi1uzind.e 
 |-  E e. _V
2 opfi1uzind.f 
 |-  F e. _V
3 opfi1uzind.l 
 |-  L e. NN0
4 opfi1uzind.1 
 |-  ( ( v = V /\ e = E ) -> ( ps <-> ph ) )
5 opfi1uzind.2 
 |-  ( ( v = w /\ e = f ) -> ( ps <-> th ) )
6 opfi1uzind.3 
 |-  ( ( <. v , e >. e. G /\ n e. v ) -> <. ( v \ { n } ) , F >. e. G )
7 opfi1uzind.4 
 |-  ( ( w = ( v \ { n } ) /\ f = F ) -> ( th <-> ch ) )
8 opfi1uzind.base 
 |-  ( ( <. v , e >. e. G /\ ( # ` v ) = L ) -> ps )
9 opfi1uzind.step 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
10 1 a1i 
 |-  ( a = V -> E e. _V )
11 opeq12 
 |-  ( ( a = V /\ b = E ) -> <. a , b >. = <. V , E >. )
12 11 eleq1d 
 |-  ( ( a = V /\ b = E ) -> ( <. a , b >. e. G <-> <. V , E >. e. G ) )
13 10 12 sbcied 
 |-  ( a = V -> ( [. E / b ]. <. a , b >. e. G <-> <. V , E >. e. G ) )
14 13 sbcieg 
 |-  ( V e. Fin -> ( [. V / a ]. [. E / b ]. <. a , b >. e. G <-> <. V , E >. e. G ) )
15 14 biimparc 
 |-  ( ( <. V , E >. e. G /\ V e. Fin ) -> [. V / a ]. [. E / b ]. <. a , b >. e. G )
16 15 3adant3 
 |-  ( ( <. V , E >. e. G /\ V e. Fin /\ L <_ ( # ` V ) ) -> [. V / a ]. [. E / b ]. <. a , b >. e. G )
17 vex 
 |-  v e. _V
18 vex 
 |-  e e. _V
19 opeq12 
 |-  ( ( a = v /\ b = e ) -> <. a , b >. = <. v , e >. )
20 19 eleq1d 
 |-  ( ( a = v /\ b = e ) -> ( <. a , b >. e. G <-> <. v , e >. e. G ) )
21 17 18 20 sbc2ie 
 |-  ( [. v / a ]. [. e / b ]. <. a , b >. e. G <-> <. v , e >. e. G )
22 21 6 sylanb 
 |-  ( ( [. v / a ]. [. e / b ]. <. a , b >. e. G /\ n e. v ) -> <. ( v \ { n } ) , F >. e. G )
23 17 difexi 
 |-  ( v \ { n } ) e. _V
24 opeq12 
 |-  ( ( a = ( v \ { n } ) /\ b = F ) -> <. a , b >. = <. ( v \ { n } ) , F >. )
25 24 eleq1d 
 |-  ( ( a = ( v \ { n } ) /\ b = F ) -> ( <. a , b >. e. G <-> <. ( v \ { n } ) , F >. e. G ) )
26 23 2 25 sbc2ie 
 |-  ( [. ( v \ { n } ) / a ]. [. F / b ]. <. a , b >. e. G <-> <. ( v \ { n } ) , F >. e. G )
27 22 26 sylibr 
 |-  ( ( [. v / a ]. [. e / b ]. <. a , b >. e. G /\ n e. v ) -> [. ( v \ { n } ) / a ]. [. F / b ]. <. a , b >. e. G )
28 21 8 sylanb 
 |-  ( ( [. v / a ]. [. e / b ]. <. a , b >. e. G /\ ( # ` v ) = L ) -> ps )
29 21 3anbi1i 
 |-  ( ( [. v / a ]. [. e / b ]. <. a , b >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) <-> ( <. v , e >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) )
30 29 anbi2i 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( [. v / a ]. [. e / b ]. <. a , b >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) <-> ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) )
31 30 9 sylanb 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( [. v / a ]. [. e / b ]. <. a , b >. e. G /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
32 2 3 4 5 27 7 28 31 fi1uzind 
 |-  ( ( [. V / a ]. [. E / b ]. <. a , b >. e. G /\ V e. Fin /\ L <_ ( # ` V ) ) -> ph )
33 16 32 syld3an1 
 |-  ( ( <. V , E >. e. G /\ V e. Fin /\ L <_ ( # ` V ) ) -> ph )