grimuhgr - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > grimuhgr		Structured version Visualization version GIF version

Theorem grimuhgr 47878

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.)

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

Proof of Theorem grimuhgr Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2737	. . . . . . 7 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
2		eqid 2737	. . . . . . 7 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
3		eqid 2737	. . . . . . 7 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
4		eqid 2737	. . . . . . 7 ⊢ (iEdg‘𝑇) = (iEdg‘𝑇)
5	1, 2, 3, 4	grimprop 47869	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))))
6		fdmrn 6767	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝑇) ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇))
7	6	biimpi 216	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝑇) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇))
8	7	3ad2ant3 1136	. . . . . . . . . . . 12 ⊢ ((𝐹:(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 480	. . . . . . . . . . 11 ⊢ (((𝐹:(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 6596	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝑇) ↔ (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
11	10	biimpi 216	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝑇) → (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
12	11	3ad2ant3 1136	. . . . . . . . . . . 12 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) ∧ Fun (iEdg‘𝑇)) → (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
13		f1ofo 6855	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) → 𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇))
14	13	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → 𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇))
15	14	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹:(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 6970	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)
17	15, 16	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:(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 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:(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 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑇)‘(𝑗‘𝑖)) = ((iEdg‘𝑇)‘(𝑗‘𝑦)))
20		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑆)‘𝑖) = ((iEdg‘𝑆)‘𝑦))
21	20	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → (𝐹 “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))
22	19, 21	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑦 → (((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
23	22	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ dom (iEdg‘𝑆) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
24	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:(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 6850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → Fun 𝐹)
26	25	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → Fun 𝐹)
27	26	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) → Fun 𝐹)
28		fvex 6919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((iEdg‘𝑆)‘𝑦) ∈ V
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ∈ V)
30		funimaexg 6653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((Fun 𝐹 ∧ ((iEdg‘𝑆)‘𝑦) ∈ V) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V)
31	27, 29, 30	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V)
32		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → 𝐹:(Vtx‘𝑆)⟶(Vtx‘𝑇))
33	32	fimassd 6757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
34	33	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
35	34	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
36	35	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:(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 4606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ 𝒫 (Vtx‘𝑇))
38		f1odm 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → dom 𝐹 = (Vtx‘𝑆))
39	38	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → dom 𝐹 = (Vtx‘𝑆))
40	39	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → dom 𝐹 = (Vtx‘𝑆))
41	40	ineq1d 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) = ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)))
42		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}))
43	42	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (𝑦 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅})))
44	43	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅})))
45		eldifsn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
46	28	elpw 4604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆))
47	45, 46	bianbi 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
48		sseqin2 4223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ↔ ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦))
49	48	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦))
50	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦))
51		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((iEdg‘𝑆)‘𝑦) ≠ ∅)
52	50, 51	eqnetrd 3008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
53	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → ((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
54	47, 53	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
55	44, 54	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
56	55	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
57	41, 56	eqnetrd 3008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
58	57	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
59	58	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
60	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹:(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 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐹:(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 6099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
63		eldifsn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ 𝒫 (Vtx‘𝑇) ∧ (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
64	37, 62, 63	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐹:(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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹:(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 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)) → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})))
67	66	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐹:(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 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐹:(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 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = ((iEdg‘𝑇)‘𝑥))
70	69	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗‘𝑦) = 𝑥 → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})))
71	68, 70	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐹:(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 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:(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 47	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:(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 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹:(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 86	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹:(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 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:(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 1111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹:(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 3153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:(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 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:(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 3145	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:(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 1120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:(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 1120	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:(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 98	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(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 410	. . . . . . . . . . . . . 14 ⊢ (𝐹:(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 1111	. . . . . . . . . . . . 13 ⊢ ((𝐹:(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 406	. . . . . . . . . . . 12 ⊢ (((𝐹:(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 7141	. . . . . . . . . . . 12 ⊢ (((iEdg‘𝑇) Fn dom (iEdg‘𝑇) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})) → ran (iEdg‘𝑇) ⊆ (𝒫 (Vtx‘𝑇) ∖ {∅}))
88	12, 86, 87	syl2an2r 685	. . . . . . . . . . 11 ⊢ (((𝐹:(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 6753	. . . . . . . . . 10 ⊢ (((𝐹:(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 412	. . . . . . . . 9 ⊢ ((𝐹:(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 1120	. . . . . . . 8 ⊢ (𝐹:(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 1933	. . . . . . 7 ⊢ (𝐹:(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 406	. . . . . 6 ⊢ ((𝐹:(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 17	. . . . 5 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
95	94	impcom 407	. . . 4 ⊢ ((Fun (iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅})))
96		grimdmrel 47866	. . . . . . 7 ⊢ Rel dom GraphIso
97	96	ovrcl 7472	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
98	1, 3	isuhgr 29077	. . . . . . . 8 ⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
99	98	adantr 480	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
100	2, 4	isuhgr 29077	. . . . . . . 8 ⊢ (𝑇 ∈ V → (𝑇 ∈ UHGraph ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅})))
101	100	adantl 481	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑇 ∈ UHGraph ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅})))
102	99, 101	imbi12d 344	. . . . . 6 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
103	97, 102	syl 17	. . . . 5 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
104	103	adantl 481	. . . 4 ⊢ ((Fun (iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
105	95, 104	mpbird 257	. . 3 ⊢ ((Fun (iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → (𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph))
106	105	ex 412	. 2 ⊢ (Fun (iEdg‘𝑇) → (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph)))
107	106	3imp31 1112	1 ⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇) ∧ Fun (iEdg‘𝑇)) → 𝑇 ∈ UHGraph)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ∖ cdif 3948 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 𝒫 cpw 4600 {csn 4626 dom cdm 5685 ran crn 5686 “ cima 5688 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 Vtxcvtx 29013 iEdgciedg 29014 UHGraphcuhgr 29073 GraphIso cgrim 47861

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-map 8868 df-uhgr 29075 df-grim 47864

This theorem is referenced by: (None)

W3C validator