Metamath Proof Explorer

Theorem isubgr0uhgr

Description: The subgraph induced by an empty set of vertices of a hypergraph. (Contributed by AV, 13-May-2025)

Ref Expression
Assertion isubgr0uhgr ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr ∅ ) = ⟨ ∅ , ∅ ⟩ )

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 2 3 isisubgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ ∅ ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ∅ ) = ⟨ ∅ , ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) ⟩ )
5 1 4 mpan2 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr ∅ ) = ⟨ ∅ , ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) ⟩ )
6 inrab2 ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ∩ dom ( iEdg ‘ 𝐺 ) ) = { 𝑥 ∈ ( dom ( iEdg ‘ 𝐺 ) ∩ dom ( iEdg ‘ 𝐺 ) ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ }
7 inidm ⊢ ( dom ( iEdg ‘ 𝐺 ) ∩ dom ( iEdg ‘ 𝐺 ) ) = dom ( iEdg ‘ 𝐺 )
8 7 rabeqi ⊢ { 𝑥 ∈ ( dom ( iEdg ‘ 𝐺 ) ∩ dom ( iEdg ‘ 𝐺 ) ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ }
9 ss0b ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ )
10 8 9 rabbieq ⊢ { 𝑥 ∈ ( dom ( iEdg ‘ 𝐺 ) ∩ dom ( iEdg ‘ 𝐺 ) ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ }
11 6 10 eqtri ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ∩ dom ( iEdg ‘ 𝐺 ) ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ }
12 11 ineqcomi ⊢ ( dom ( iEdg ‘ 𝐺 ) ∩ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ }
13 2 3 uhgrf ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
14 ffvelcdm ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
15 eldifsni ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ≠ ∅ )
16 14 15 syl ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ≠ ∅ )
17 16 neneqd ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ¬ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ )
18 13 17 sylan ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ¬ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ )
19 18 ralrimiva ⊢ ( 𝐺 ∈ UHGraph → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ )
20 rabeq0 ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ } = ∅ ↔ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ )
21 19 20 sylibr ⊢ ( 𝐺 ∈ UHGraph → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ∅ } = ∅ )
22 12 21 eqtrid ⊢ ( 𝐺 ∈ UHGraph → ( dom ( iEdg ‘ 𝐺 ) ∩ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = ∅ )
23 3 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
24 23 funfnd ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
25 fnresdisj ⊢ ( ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) → ( ( dom ( iEdg ‘ 𝐺 ) ∩ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = ∅ ↔ ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = ∅ ) )
26 24 25 syl ⊢ ( 𝐺 ∈ UHGraph → ( ( dom ( iEdg ‘ 𝐺 ) ∩ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = ∅ ↔ ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = ∅ ) )
27 22 26 mpbid ⊢ ( 𝐺 ∈ UHGraph → ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) = ∅ )
28 27 opeq2d ⊢ ( 𝐺 ∈ UHGraph → ⟨ ∅ , ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ ∅ } ) ⟩ = ⟨ ∅ , ∅ ⟩ )
29 5 28 eqtrd ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr ∅ ) = ⟨ ∅ , ∅ ⟩ )