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 )