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 47762

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 2740	. . . . . . 7 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
2		eqid 2740	. . . . . . 7 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
3		eqid 2740	. . . . . . 7 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
4		eqid 2740	. . . . . . 7 ⊢ (iEdg‘𝑇) = (iEdg‘𝑇)
5	1, 2, 3, 4	grimprop 47753	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))))
6		fdmrn 6779	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝑇) ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇))
7	6	biimpi 216	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝑇) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇))
8	7	3ad2ant3 1135	. . . . . . . . . . . 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 6608	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝑇) ↔ (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
11	10	biimpi 216	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝑇) → (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
12	11	3ad2ant3 1135	. . . . . . . . . . . 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 6869	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) → 𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇))
14	13	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . . . . . . . . . . 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 6983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)
17	15, 16	sylan 579	. . . . . . . . . . . . . . . . . . . . 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 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑇)‘(𝑗‘𝑖)) = ((iEdg‘𝑇)‘(𝑗‘𝑦)))
20		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑆)‘𝑖) = ((iEdg‘𝑆)‘𝑦))
21	20	imaeq2d 6089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → (𝐹 “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))
22	19, 21	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑦 → (((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
23	22	rspcv 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → Fun 𝐹)
26	25	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((Fun 𝐹 ∧ ((iEdg‘𝑆)‘𝑦) ∈ V) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V)
31	27, 29, 30	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → 𝐹:(Vtx‘𝑆)⟶(Vtx‘𝑇))
33	32	fimassd 6768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
34	33	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) = ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)))
42		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
46	28	elpw 4626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆))
47	45, 46	bianbi 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
48		sseqin2 4244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
63		eldifsn 4811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ 𝒫 (Vtx‘𝑇) ∧ (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
64	37, 62, 63	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = ((iEdg‘𝑇)‘𝑥))
70	69	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3159	. . . . . . . . . . . . . . . . . . . 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 3151	. . . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . 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 7155	. . . . . . . . . . . 12 ⊢ (((iEdg‘𝑇) Fn dom (iEdg‘𝑇) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})) → ran (iEdg‘𝑇) ⊆ (𝒫 (Vtx‘𝑇) ∖ {∅}))
88	12, 86, 87	syl2an2r 684	. . . . . . . . . . 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 6764	. . . . . . . . . 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 1119	. . . . . . . 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 1932	. . . . . . 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 47750	. . . . . . 7 ⊢ Rel dom GraphIso
97	96	ovrcl 7489	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
98	1, 3	isuhgr 29095	. . . . . . . 8 ⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
99	98	adantr 480	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
100	2, 4	isuhgr 29095	. . . . . . . 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 1537 ∃wex 1777 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 Vcvv 3488 ∖ cdif 3973 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 𝒫 cpw 4622 {csn 4648 dom cdm 5700 ran crn 5701 “ cima 5703 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 –onto→wfo 6571 –1-1-onto→wf1o 6572 ‘cfv 6573 (class class class)co 7448 Vtxcvtx 29031 iEdgciedg 29032 UHGraphcuhgr 29091 GraphIso cgrim 47745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-sbc 3805 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-ov 7451 df-oprab 7452 df-mpo 7453 df-map 8886 df-uhgr 29093 df-grim 47748

This theorem is referenced by: (None)

W3C validator