# 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 ( 𝐺 ∈ Plig → ⟨ 𝐺 , ( I ↾ 𝐺 ) ⟩ ∈ UHGraph )

### Proof

Step Hyp Ref Expression
1 f1oi ( I ↾ 𝐺 ) : 𝐺1-1-onto𝐺
2 f1of ( ( I ↾ 𝐺 ) : 𝐺1-1-onto𝐺 → ( I ↾ 𝐺 ) : 𝐺𝐺 )
3 pwuni 𝐺 ⊆ 𝒫 𝐺
4 n0lplig ( 𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺 )
5 4 adantr ( ( 𝐺 ∈ Plig ∧ 𝐺 ⊆ 𝒫 𝐺 ) → ¬ ∅ ∈ 𝐺 )
6 disjsn ( ( 𝐺 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ 𝐺 )
7 5 6 sylibr ( ( 𝐺 ∈ Plig ∧ 𝐺 ⊆ 𝒫 𝐺 ) → ( 𝐺 ∩ { ∅ } ) = ∅ )
8 reldisj ( 𝐺 ⊆ 𝒫 𝐺 → ( ( 𝐺 ∩ { ∅ } ) = ∅ ↔ 𝐺 ⊆ ( 𝒫 𝐺 ∖ { ∅ } ) ) )
9 8 adantl ( ( 𝐺 ∈ Plig ∧ 𝐺 ⊆ 𝒫 𝐺 ) → ( ( 𝐺 ∩ { ∅ } ) = ∅ ↔ 𝐺 ⊆ ( 𝒫 𝐺 ∖ { ∅ } ) ) )
10 7 9 mpbid ( ( 𝐺 ∈ Plig ∧ 𝐺 ⊆ 𝒫 𝐺 ) → 𝐺 ⊆ ( 𝒫 𝐺 ∖ { ∅ } ) )
11 3 10 mpan2 ( 𝐺 ∈ Plig → 𝐺 ⊆ ( 𝒫 𝐺 ∖ { ∅ } ) )
12 fss ( ( ( I ↾ 𝐺 ) : 𝐺𝐺𝐺 ⊆ ( 𝒫 𝐺 ∖ { ∅ } ) ) → ( I ↾ 𝐺 ) : 𝐺 ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) )
13 11 12 sylan2 ( ( ( I ↾ 𝐺 ) : 𝐺𝐺𝐺 ∈ Plig ) → ( I ↾ 𝐺 ) : 𝐺 ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) )
14 13 ex ( ( I ↾ 𝐺 ) : 𝐺𝐺 → ( 𝐺 ∈ Plig → ( I ↾ 𝐺 ) : 𝐺 ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) ) )
15 1 2 14 mp2b ( 𝐺 ∈ Plig → ( I ↾ 𝐺 ) : 𝐺 ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) )
16 15 ffdmd ( 𝐺 ∈ Plig → ( I ↾ 𝐺 ) : dom ( I ↾ 𝐺 ) ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) )
17 uniexg ( 𝐺 ∈ Plig → 𝐺 ∈ V )
18 resiexg ( 𝐺 ∈ Plig → ( I ↾ 𝐺 ) ∈ V )
19 isuhgrop ( ( 𝐺 ∈ V ∧ ( I ↾ 𝐺 ) ∈ V ) → ( ⟨ 𝐺 , ( I ↾ 𝐺 ) ⟩ ∈ UHGraph ↔ ( I ↾ 𝐺 ) : dom ( I ↾ 𝐺 ) ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) ) )
20 17 18 19 syl2anc ( 𝐺 ∈ Plig → ( ⟨ 𝐺 , ( I ↾ 𝐺 ) ⟩ ∈ UHGraph ↔ ( I ↾ 𝐺 ) : dom ( I ↾ 𝐺 ) ⟶ ( 𝒫 𝐺 ∖ { ∅ } ) ) )
21 16 20 mpbird ( 𝐺 ∈ Plig → ⟨ 𝐺 , ( I ↾ 𝐺 ) ⟩ ∈ UHGraph )