Metamath Proof Explorer

Theorem isubgredg

Description: An edge of an induced subgraph of a hypergraph is an edge of the hypergraph connecting vertices of the subgraph. (Contributed by AV, 24-Sep-2025)

Ref Expression
Hypotheses isubgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
isubgredg.h ⊢ 𝐻 = ( 𝐺 ISubGr 𝑆 )
isubgredg.i ⊢ 𝐼 = ( Edg ‘ 𝐻 )
Assertion isubgredg ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ 𝐼 ↔ ( 𝐾 ∈ 𝐸 ∧ 𝐾 ⊆ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isubgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 isubgredg.h ⊢ 𝐻 = ( 𝐺 ISubGr 𝑆 )
4 isubgredg.i ⊢ 𝐼 = ( Edg ‘ 𝐻 )
5 3 fveq2i ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) )
6 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7 1 6 isubgriedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) )
8 5 7 eqtrid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ 𝐻 ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) )
9 8 rneqd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ran ( iEdg ‘ 𝐻 ) = ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) )
10 9 eleq2d ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ ran ( iEdg ‘ 𝐻 ) ↔ 𝐾 ∈ ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ) )
11 1 6 uhgrf ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
12 11 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
13 12 ffnd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
14 ssrab2 ⊢ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 )
15 14 a1i ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 ) )
16 13 15 fnssresd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) Fn { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } )
17 fvelrnb ⊢ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) Fn { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } → ( 𝐾 ∈ ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ↔ ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
18 16 17 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ↔ ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
19 fvres ⊢ ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } → ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
20 19 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
21 20 eqeq1d ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 ) )
22 fveq2 ⊢ ( 𝑖 = 𝑥 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
23 22 sseq1d ⊢ ( 𝑖 = 𝑥 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
24 23 elrab ⊢ ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ↔ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
25 6 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
26 25 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → Fun ( iEdg ‘ 𝐺 ) )
27 simpl ⊢ ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) → 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) )
28 fvelrn ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) )
29 26 27 28 syl2anr ⊢ ( ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) )
30 simpr ⊢ ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 )
31 30 adantr ⊢ ( ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 )
32 29 31 jca ⊢ ( ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
33 32 ex ⊢ ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) ) )
34 24 33 sylbi ⊢ ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } → ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) ) )
35 34 impcom ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
36 eleq1 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) ↔ 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ) )
37 sseq1 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ↔ 𝐾 ⊆ 𝑆 ) )
38 36 37 anbi12d ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 → ( ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) ↔ ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
39 35 38 syl5ibcom ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
40 21 39 sylbid ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
41 40 rexlimdva ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
42 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
43 42 eqcomi ⊢ ran ( iEdg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
44 43 eleq2i ⊢ ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ↔ 𝐾 ∈ ( Edg ‘ 𝐺 ) )
45 6 edgiedgb ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
46 44 45 bitrid ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
47 25 46 syl ⊢ ( 𝐺 ∈ UHGraph → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
48 47 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
49 simprl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) )
50 simpr ⊢ ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
51 50 sseq1d ⊢ ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( 𝐾 ⊆ 𝑆 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
52 51 biimpcd ⊢ ( 𝐾 ⊆ 𝑆 → ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
53 52 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) → ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ) )
54 53 imp ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 )
55 49 54 24 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) → 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } )
56 simpr ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } )
57 50 eqcomd ⊢ ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 )
58 57 adantl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = 𝐾 )
59 19 58 sylan9eqr ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 )
60 56 59 jca ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ∧ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) → ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ∧ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
61 55 60 mpdan ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ∧ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
62 61 ex ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) → ( ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ∧ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) ) )
63 62 eximdv ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) → ( ∃ 𝑥 ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) → ∃ 𝑥 ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ∧ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) ) )
64 df-rex ⊢ ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
65 df-rex ⊢ ( ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ∧ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
66 63 64 65 3imtr4g ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝐾 ⊆ 𝑆 ) → ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
67 66 ex ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ⊆ 𝑆 → ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) ) )
68 67 com23 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝐾 ⊆ 𝑆 → ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) ) )
69 48 68 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) → ( 𝐾 ⊆ 𝑆 → ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) ) )
70 69 impd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ) )
71 41 70 impbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ∃ 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑆 } ) ‘ 𝑥 ) = 𝐾 ↔ ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
72 10 18 71 3bitrd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ ran ( iEdg ‘ 𝐻 ) ↔ ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
73 edgval ⊢ ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 )
74 4 73 eqtri ⊢ 𝐼 = ran ( iEdg ‘ 𝐻 )
75 74 eleq2i ⊢ ( 𝐾 ∈ 𝐼 ↔ 𝐾 ∈ ran ( iEdg ‘ 𝐻 ) )
76 2 42 eqtri ⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
77 76 eleq2i ⊢ ( 𝐾 ∈ 𝐸 ↔ 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) )
78 77 anbi1i ⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝐾 ⊆ 𝑆 ) ↔ ( 𝐾 ∈ ran ( iEdg ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) )
79 72 75 78 3bitr4g ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ 𝐼 ↔ ( 𝐾 ∈ 𝐸 ∧ 𝐾 ⊆ 𝑆 ) ) )