Metamath Proof Explorer

Theorem isubgr0uhgr

Description: The subgraph induced by an empty set of vertices of a hypergraph. (Contributed by AV, 13-May-2025)

Ref Expression
Assertion isubgr0uhgr 
|- ( G e. UHGraph -> ( G ISubGr (/) ) = <. (/) , (/) >. )

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ ( Vtx ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 2 3 isisubgr 
 |-  ( ( G e. UHGraph /\ (/) C_ ( Vtx ` G ) ) -> ( G ISubGr (/) ) = <. (/) , ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) >. )
5 1 4 mpan2 
 |-  ( G e. UHGraph -> ( G ISubGr (/) ) = <. (/) , ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) >. )
6 inrab2 
 |-  ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } i^i dom ( iEdg ` G ) ) = { x e. ( dom ( iEdg ` G ) i^i dom ( iEdg ` G ) ) | ( ( iEdg ` G ) ` x ) C_ (/) }
7 inidm 
 |-  ( dom ( iEdg ` G ) i^i dom ( iEdg ` G ) ) = dom ( iEdg ` G )
8 7 rabeqi 
 |-  { x e. ( dom ( iEdg ` G ) i^i dom ( iEdg ` G ) ) | ( ( iEdg ` G ) ` x ) C_ (/) } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) }
9 ss0b 
 |-  ( ( ( iEdg ` G ) ` x ) C_ (/) <-> ( ( iEdg ` G ) ` x ) = (/) )
10 8 9 rabbieq 
 |-  { x e. ( dom ( iEdg ` G ) i^i dom ( iEdg ` G ) ) | ( ( iEdg ` G ) ` x ) C_ (/) } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = (/) }
11 6 10 eqtri 
 |-  ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } i^i dom ( iEdg ` G ) ) = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = (/) }
12 11 ineqcomi 
 |-  ( dom ( iEdg ` G ) i^i { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = (/) }
13 2 3 uhgrf 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) )
14 ffvelcdm 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) /\ x e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` x ) e. ( ~P ( Vtx ` G ) \ { (/) } ) )
15 eldifsni 
 |-  ( ( ( iEdg ` G ) ` x ) e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( ( iEdg ` G ) ` x ) =/= (/) )
16 14 15 syl 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) /\ x e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` x ) =/= (/) )
17 16 neneqd 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) /\ x e. dom ( iEdg ` G ) ) -> -. ( ( iEdg ` G ) ` x ) = (/) )
18 13 17 sylan 
 |-  ( ( G e. UHGraph /\ x e. dom ( iEdg ` G ) ) -> -. ( ( iEdg ` G ) ` x ) = (/) )
19 18 ralrimiva 
 |-  ( G e. UHGraph -> A. x e. dom ( iEdg ` G ) -. ( ( iEdg ` G ) ` x ) = (/) )
20 rabeq0 
 |-  ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = (/) } = (/) <-> A. x e. dom ( iEdg ` G ) -. ( ( iEdg ` G ) ` x ) = (/) )
21 19 20 sylibr 
 |-  ( G e. UHGraph -> { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = (/) } = (/) )
22 12 21 eqtrid 
 |-  ( G e. UHGraph -> ( dom ( iEdg ` G ) i^i { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = (/) )
23 3 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
24 23 funfnd 
 |-  ( G e. UHGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
25 fnresdisj 
 |-  ( ( iEdg ` G ) Fn dom ( iEdg ` G ) -> ( ( dom ( iEdg ` G ) i^i { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = (/) <-> ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = (/) ) )
26 24 25 syl 
 |-  ( G e. UHGraph -> ( ( dom ( iEdg ` G ) i^i { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = (/) <-> ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = (/) ) )
27 22 26 mpbid 
 |-  ( G e. UHGraph -> ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) = (/) )
28 27 opeq2d 
 |-  ( G e. UHGraph -> <. (/) , ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ (/) } ) >. = <. (/) , (/) >. )
29 5 28 eqtrd 
 |-  ( G e. UHGraph -> ( G ISubGr (/) ) = <. (/) , (/) >. )