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 ∈ Plig → ⋃ G I ↾ G ∈ 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 ⊆ 𝒫 ⋃ G
4 n0lplig ⊢ G ∈ Plig → ¬ ∅ ∈ G
5 4 adantr ⊢ G ∈ Plig ∧ G ⊆ 𝒫 ⋃ G → ¬ ∅ ∈ G
6 disjsn ⊢ G ∩ ∅ = ∅ ↔ ¬ ∅ ∈ G
7 5 6 sylibr ⊢ G ∈ Plig ∧ G ⊆ 𝒫 ⋃ G → G ∩ ∅ = ∅
8 reldisj ⊢ G ⊆ 𝒫 ⋃ G → G ∩ ∅ = ∅ ↔ G ⊆ 𝒫 ⋃ G ∖ ∅
9 8 adantl ⊢ G ∈ Plig ∧ G ⊆ 𝒫 ⋃ G → G ∩ ∅ = ∅ ↔ G ⊆ 𝒫 ⋃ G ∖ ∅
10 7 9 mpbid ⊢ G ∈ Plig ∧ G ⊆ 𝒫 ⋃ G → G ⊆ 𝒫 ⋃ G ∖ ∅
11 3 10 mpan2 ⊢ G ∈ Plig → G ⊆ 𝒫 ⋃ G ∖ ∅
12 fss ⊢ I ↾ G : G ⟶ G ∧ G ⊆ 𝒫 ⋃ G ∖ ∅ → I ↾ G : G ⟶ 𝒫 ⋃ G ∖ ∅
13 11 12 sylan2 ⊢ I ↾ G : G ⟶ G ∧ G ∈ Plig → I ↾ G : G ⟶ 𝒫 ⋃ G ∖ ∅
14 13 ex ⊢ I ↾ G : G ⟶ G → G ∈ Plig → I ↾ G : G ⟶ 𝒫 ⋃ G ∖ ∅
15 1 2 14 mp2b ⊢ G ∈ Plig → I ↾ G : G ⟶ 𝒫 ⋃ G ∖ ∅
16 15 ffdmd ⊢ G ∈ Plig → I ↾ G : dom ⁡ I ↾ G ⟶ 𝒫 ⋃ G ∖ ∅
17 uniexg ⊢ G ∈ Plig → ⋃ G ∈ V
18 resiexg ⊢ G ∈ Plig → I ↾ G ∈ V
19 isuhgrop ⊢ ⋃ G ∈ V ∧ I ↾ G ∈ V → ⋃ G I ↾ G ∈ UHGraph ↔ I ↾ G : dom ⁡ I ↾ G ⟶ 𝒫 ⋃ G ∖ ∅
20 17 18 19 syl2anc ⊢ G ∈ Plig → ⋃ G I ↾ G ∈ UHGraph ↔ I ↾ G : dom ⁡ I ↾ G ⟶ 𝒫 ⋃ G ∖ ∅
21 16 20 mpbird ⊢ G ∈ Plig → ⋃ G I ↾ G ∈ UHGraph