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

Proof

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

Metamath Proof Explorer

Theorem pliguhgr

Proof