# Metamath Proof Explorer

## 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}\in \mathrm{Plig}\to ⟨\bigcup {G},{\mathrm{I}↾}_{{G}}⟩\in \mathrm{UHGraph}$

### Proof

Step Hyp Ref Expression
1 f1oi ${⊢}\left({\mathrm{I}↾}_{{G}}\right):{G}\underset{1-1 onto}{⟶}{G}$
2 f1of ${⊢}\left({\mathrm{I}↾}_{{G}}\right):{G}\underset{1-1 onto}{⟶}{G}\to \left({\mathrm{I}↾}_{{G}}\right):{G}⟶{G}$
3 pwuni ${⊢}{G}\subseteq 𝒫\bigcup {G}$
4 n0lplig ${⊢}{G}\in \mathrm{Plig}\to ¬\varnothing \in {G}$
5 4 adantr ${⊢}\left({G}\in \mathrm{Plig}\wedge {G}\subseteq 𝒫\bigcup {G}\right)\to ¬\varnothing \in {G}$
6 disjsn ${⊢}{G}\cap \left\{\varnothing \right\}=\varnothing ↔¬\varnothing \in {G}$
7 5 6 sylibr ${⊢}\left({G}\in \mathrm{Plig}\wedge {G}\subseteq 𝒫\bigcup {G}\right)\to {G}\cap \left\{\varnothing \right\}=\varnothing$
8 reldisj ${⊢}{G}\subseteq 𝒫\bigcup {G}\to \left({G}\cap \left\{\varnothing \right\}=\varnothing ↔{G}\subseteq 𝒫\bigcup {G}\setminus \left\{\varnothing \right\}\right)$
9 8 adantl ${⊢}\left({G}\in \mathrm{Plig}\wedge {G}\subseteq 𝒫\bigcup {G}\right)\to \left({G}\cap \left\{\varnothing \right\}=\varnothing ↔{G}\subseteq 𝒫\bigcup {G}\setminus \left\{\varnothing \right\}\right)$
10 7 9 mpbid ${⊢}\left({G}\in \mathrm{Plig}\wedge {G}\subseteq 𝒫\bigcup {G}\right)\to {G}\subseteq 𝒫\bigcup {G}\setminus \left\{\varnothing \right\}$
11 3 10 mpan2 ${⊢}{G}\in \mathrm{Plig}\to {G}\subseteq 𝒫\bigcup {G}\setminus \left\{\varnothing \right\}$
12 fss ${⊢}\left(\left({\mathrm{I}↾}_{{G}}\right):{G}⟶{G}\wedge {G}\subseteq 𝒫\bigcup {G}\setminus \left\{\varnothing \right\}\right)\to \left({\mathrm{I}↾}_{{G}}\right):{G}⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}$
13 11 12 sylan2 ${⊢}\left(\left({\mathrm{I}↾}_{{G}}\right):{G}⟶{G}\wedge {G}\in \mathrm{Plig}\right)\to \left({\mathrm{I}↾}_{{G}}\right):{G}⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}$
14 13 ex ${⊢}\left({\mathrm{I}↾}_{{G}}\right):{G}⟶{G}\to \left({G}\in \mathrm{Plig}\to \left({\mathrm{I}↾}_{{G}}\right):{G}⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}\right)$
15 1 2 14 mp2b ${⊢}{G}\in \mathrm{Plig}\to \left({\mathrm{I}↾}_{{G}}\right):{G}⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}$
16 15 ffdmd ${⊢}{G}\in \mathrm{Plig}\to \left({\mathrm{I}↾}_{{G}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{G}}\right)⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}$
17 uniexg ${⊢}{G}\in \mathrm{Plig}\to \bigcup {G}\in \mathrm{V}$
18 resiexg ${⊢}{G}\in \mathrm{Plig}\to {\mathrm{I}↾}_{{G}}\in \mathrm{V}$
19 isuhgrop ${⊢}\left(\bigcup {G}\in \mathrm{V}\wedge {\mathrm{I}↾}_{{G}}\in \mathrm{V}\right)\to \left(⟨\bigcup {G},{\mathrm{I}↾}_{{G}}⟩\in \mathrm{UHGraph}↔\left({\mathrm{I}↾}_{{G}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{G}}\right)⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}\right)$
20 17 18 19 syl2anc ${⊢}{G}\in \mathrm{Plig}\to \left(⟨\bigcup {G},{\mathrm{I}↾}_{{G}}⟩\in \mathrm{UHGraph}↔\left({\mathrm{I}↾}_{{G}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{G}}\right)⟶𝒫\bigcup {G}\setminus \left\{\varnothing \right\}\right)$
21 16 20 mpbird ${⊢}{G}\in \mathrm{Plig}\to ⟨\bigcup {G},{\mathrm{I}↾}_{{G}}⟩\in \mathrm{UHGraph}$