Theorem pliguhgr

Description: Any planar incidence geometry G can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr for a generalization of this case for arbitrary incidence structures (planar incidence geometries are such incidence structures). (Proposed by Gerard Lang, 24-Nov-2021.) (Contributed by AV, 28-Nov-2021)

	Ref	Expression
Assertion	pliguhgr	|- ( G e. Plig -> <. U. G , ( _I |` G ) >. e. UHGraph )

Proof

Step	Hyp	Ref	Expression
1		f1oi	|- ( _I |` G ) : G -1-1-onto-> G
2		f1of	|- ( ( _I |` G ) : G -1-1-onto-> G -> ( _I |` G ) : G --> G )
3		pwuni	|- G C_ ~P U. G
4		n0lplig	|- ( G e. Plig -> -. (/) e. G )
5	4	adantr	|- ( ( G e. Plig /\ G C_ ~P U. G ) -> -. (/) e. G )
6		disjsn	|- ( ( G i^i { (/) } ) = (/) <-> -. (/) e. G )
7	5 6	sylibr	|- ( ( G e. Plig /\ G C_ ~P U. G ) -> ( G i^i { (/) } ) = (/) )
8		reldisj	|- ( G C_ ~P U. G -> ( ( G i^i { (/) } ) = (/) <-> G C_ ( ~P U. G \ { (/) } ) ) )
9	8	adantl	|- ( ( G e. Plig /\ G C_ ~P U. G ) -> ( ( G i^i { (/) } ) = (/) <-> G C_ ( ~P U. G \ { (/) } ) ) )
10	7 9	mpbid	|- ( ( G e. Plig /\ G C_ ~P U. G ) -> G C_ ( ~P U. G \ { (/) } ) )
11	3 10	mpan2	|- ( G e. Plig -> G C_ ( ~P U. G \ { (/) } ) )
12		fss	|- ( ( ( _I |` G ) : G --> G /\ G C_ ( ~P U. G \ { (/) } ) ) -> ( _I |` G ) : G --> ( ~P U. G \ { (/) } ) )
13	11 12	sylan2	|- ( ( ( _I |` G ) : G --> G /\ G e. Plig ) -> ( _I |` G ) : G --> ( ~P U. G \ { (/) } ) )
14	13	ex	|- ( ( _I |` G ) : G --> G -> ( G e. Plig -> ( _I |` G ) : G --> ( ~P U. G \ { (/) } ) ) )
15	1 2 14	mp2b	|- ( G e. Plig -> ( _I |` G ) : G --> ( ~P U. G \ { (/) } ) )
16	15	ffdmd	|- ( G e. Plig -> ( _I |` G ) : dom ( _I |` G ) --> ( ~P U. G \ { (/) } ) )
17		uniexg	|- ( G e. Plig -> U. G e. _V )
18		resiexg	|- ( G e. Plig -> ( _I |` G ) e. _V )
19		isuhgrop	|- ( ( U. G e. _V /\ ( _I |` G ) e. _V ) -> ( <. U. G , ( _I |` G ) >. e. UHGraph <-> ( _I |` G ) : dom ( _I |` G ) --> ( ~P U. G \ { (/) } ) ) )
20	17 18 19	syl2anc	|- ( G e. Plig -> ( <. U. G , ( _I |` G ) >. e. UHGraph <-> ( _I |` G ) : dom ( _I |` G ) --> ( ~P U. G \ { (/) } ) ) )
21	16 20	mpbird	|- ( G e. Plig -> <. U. G , ( _I |` G ) >. e. UHGraph )