Metamath Proof Explorer

Theorem grimuhgr

Description: If there is a graph isomorphism between a hypergraph and a class with an edge function, the class is also a hypergraph. (Contributed by AV, 2-May-2025)

Ref Expression
Assertion grimuhgr ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → 𝑇 ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
2 eqid ⊢ ( Vtx ‘ 𝑇 ) = ( Vtx ‘ 𝑇 )
3 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
4 eqid ⊢ ( iEdg ‘ 𝑇 ) = ( iEdg ‘ 𝑇 )
5 1 2 3 4 grimprop ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) )
6 fdmrn ⊢ ( Fun ( iEdg ‘ 𝑇 ) ↔ ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ran ( iEdg ‘ 𝑇 ) )
7 6 biimpi ⊢ ( Fun ( iEdg ‘ 𝑇 ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ran ( iEdg ‘ 𝑇 ) )
8 7 3ad2ant3 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ran ( iEdg ‘ 𝑇 ) )
9 8 adantr ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ran ( iEdg ‘ 𝑇 ) )
10 funfn ⊢ ( Fun ( iEdg ‘ 𝑇 ) ↔ ( iEdg ‘ 𝑇 ) Fn dom ( iEdg ‘ 𝑇 ) )
11 10 biimpi ⊢ ( Fun ( iEdg ‘ 𝑇 ) → ( iEdg ‘ 𝑇 ) Fn dom ( iEdg ‘ 𝑇 ) )
12 11 3ad2ant3 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( iEdg ‘ 𝑇 ) Fn dom ( iEdg ‘ 𝑇 ) )
13 f1ofo ⊢ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) )
14 13 3ad2ant2 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) )
15 14 3ad2ant1 ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) )
16 foelcdmi ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 )
17 15 16 sylan ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 )
18 17 ex ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 ) )
19 2fveq3 ⊢ ( 𝑖 = 𝑦 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) )
20 fveq2 ⊢ ( 𝑖 = 𝑦 → ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
21 20 imaeq2d ⊢ ( 𝑖 = 𝑦 → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) )
22 19 21 eqeq12d ⊢ ( 𝑖 = 𝑦 → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
23 22 rspcv ⊢ ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
24 23 adantl ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
25 f1ofun ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → Fun 𝐹 )
26 25 3ad2ant1 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → Fun 𝐹 )
27 26 adantr ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → Fun 𝐹 )
28 fvex ⊢ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ V
29 28 a1i ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ V )
30 funimaexg ⊢ ( ( Fun 𝐹 ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ V ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ V )
31 27 29 30 syl2an2r ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ V )
32 f1of ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → 𝐹 : ( Vtx ‘ 𝑆 ) ⟶ ( Vtx ‘ 𝑇 ) )
33 32 fimassd ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝑇 ) )
34 33 3ad2ant1 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝑇 ) )
35 34 adantr ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝑇 ) )
36 35 adantr ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝑇 ) )
37 31 36 elpwd ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ 𝒫 ( Vtx ‘ 𝑇 ) )
38 f1odm ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → dom 𝐹 = ( Vtx ‘ 𝑆 ) )
39 38 adantr ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → dom 𝐹 = ( Vtx ‘ 𝑆 ) )
40 39 adantr ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → dom 𝐹 = ( Vtx ‘ 𝑆 ) )
41 40 ineq1d ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( dom 𝐹 ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) )
42 ffvelcdm ⊢ ( ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) )
43 42 ex ⊢ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) )
44 43 adantl ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) )
45 eldifsn ⊢ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ↔ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ ) )
46 28 elpw ⊢ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) ↔ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) )
47 45 46 bianbi ⊢ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ↔ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ ) )
48 sseqin2 ⊢ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ↔ ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
49 48 biimpi ⊢ ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
50 49 adantr ⊢ ( ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
51 simpr ⊢ ( ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ )
52 50 51 eqnetrd ⊢ ( ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ )
53 52 a1i ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ≠ ∅ ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
54 47 53 biimtrid ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
55 44 54 syld ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
56 55 imp ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( Vtx ‘ 𝑆 ) ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ )
57 41 56 eqnetrd ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( dom 𝐹 ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ )
58 57 ex ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( dom 𝐹 ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
59 58 3adant2 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( dom 𝐹 ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
60 59 adantr ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( dom 𝐹 ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
61 60 imp ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( dom 𝐹 ∩ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ )
62 61 imadisjlnd ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ )
63 eldifsn ⊢ ( ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ↔ ( ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ 𝒫 ( Vtx ‘ 𝑇 ) ∧ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ≠ ∅ ) )
64 37 62 63 sylanbrc ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
65 64 adantr ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
66 eleq1 ⊢ ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ↔ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
67 66 adantl ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ↔ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
68 65 67 mpbird ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
69 fveq2 ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) )
70 69 eleq1d ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ↔ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
71 68 70 syl5ibcom ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
72 71 ex ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
73 24 72 syld ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
74 73 ex ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) )
75 74 com23 ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) )
76 75 ex ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) ) )
77 76 3imp ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
78 77 rexlimdv ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
79 18 78 syld ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
80 79 ralrimiv ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
81 80 3exp ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
82 81 3exp ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) ) )
83 82 com35 ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) ) )
84 83 impd ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) )
85 84 3imp ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
86 85 imp ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
87 fnfvrnss ⊢ ( ( ( iEdg ‘ 𝑇 ) Fn dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) → ran ( iEdg ‘ 𝑇 ) ⊆ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
88 12 86 87 syl2an2r ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ran ( iEdg ‘ 𝑇 ) ⊆ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
89 9 88 fssd ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) ∧ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) )
90 89 ex ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
91 90 3exp ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) )
92 91 exlimdv ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) ) )
93 92 imp ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
94 5 93 syl ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( Fun ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
95 94 impcom ⊢ ( ( Fun ( iEdg ‘ 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
96 grimdmrel ⊢ Rel dom GraphIso
97 96 ovrcl ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
98 1 3 isuhgr ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ UHGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) )
99 98 adantr ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑆 ∈ UHGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) ) )
100 2 4 isuhgr ⊢ ( 𝑇 ∈ V → ( 𝑇 ∈ UHGraph ↔ ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
101 100 adantl ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑇 ∈ UHGraph ↔ ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) )
102 99 101 imbi12d ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( ( 𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph ) ↔ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
103 97 102 syl ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( ( 𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph ) ↔ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
104 103 adantl ⊢ ( ( Fun ( iEdg ‘ 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( ( 𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph ) ↔ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑆 ) ∖ { ∅ } ) → ( iEdg ‘ 𝑇 ) : dom ( iEdg ‘ 𝑇 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑇 ) ∖ { ∅ } ) ) ) )
105 95 104 mpbird ⊢ ( ( Fun ( iEdg ‘ 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph ) )
106 105 ex ⊢ ( Fun ( iEdg ‘ 𝑇 ) → ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph ) ) )
107 106 3imp31 ⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ∧ Fun ( iEdg ‘ 𝑇 ) ) → 𝑇 ∈ UHGraph )