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 49078

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 2760	. . . . . . 7 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
2		eqid 2760	. . . . . . 7 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
3		eqid 2760	. . . . . . 7 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
4		eqid 2760	. . . . . . 7 ⊢ (iEdg‘𝑇) = (iEdg‘𝑇)
5	1, 2, 3, 4	grimprop 49074	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))))
6		fdmrn 6741	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝑇) ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇))
7	6	biimpi 219	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝑇) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶ran (iEdg‘𝑇))
8	7	3ad2ant3 1153	. . . . . . . . . . . 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 486	. . . . . . . . . . 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 6570	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝑇) ↔ (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
11	10	biimpi 219	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝑇) → (iEdg‘𝑇) Fn dom (iEdg‘𝑇))
12	11	3ad2ant3 1153	. . . . . . . . . . . 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 6832	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) → 𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇))
14	13	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . 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 1151	. . . . . . . . . . . . . . . . . . . . . 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 6946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)
17	15, 16	sylan 592	. . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . 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 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑇)‘(𝑗‘𝑖)) = ((iEdg‘𝑇)‘(𝑗‘𝑦)))
20		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑆)‘𝑖) = ((iEdg‘𝑆)‘𝑦))
21	20	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → (𝐹 “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))
22	19, 21	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑦 → (((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
23	22	rspcv 3572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ dom (iEdg‘𝑆) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
24	23	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → Fun 𝐹)
26	25	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → Fun 𝐹)
27	26	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) → Fun 𝐹)
28		fvex 6898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((Fun 𝐹 ∧ ((iEdg‘𝑆)‘𝑦) ∈ V) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V)
31	27, 29, 30	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → 𝐹:(Vtx‘𝑆)⟶(Vtx‘𝑇))
33	32	fimassd 6731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
34	33	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
35	34	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ⊆ (Vtx‘𝑇))
36	35	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → dom 𝐹 = (Vtx‘𝑆))
39	38	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → dom 𝐹 = (Vtx‘𝑆))
40	39	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → dom 𝐹 = (Vtx‘𝑆))
41	40	ineq1d 4116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) = ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)))
42		ffvelcdm 7081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}))
43	42	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (𝑦 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅})))
44	43	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → ((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅})))
45		eldifsn 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
46	28	elpw 4560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆))
47	45, 46	bianbi 639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
48		sseqin2 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ↔ ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦))
49	48	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦))
50	49	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑆)‘𝑦))
51		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅) → ((iEdg‘𝑆)‘𝑦) ≠ ∅)
52	50, 51	eqnetrd 3022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
55	44, 54	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
56	55	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
57	41, 56	eqnetrd 3022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
58	57	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
59	58	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) → (𝑦 ∈ dom (iEdg‘𝑆) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
60	59	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ Fun (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅)
63		eldifsn 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ ((𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ 𝒫 (Vtx‘𝑇) ∧ (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ≠ ∅))
64	37, 62, 63	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)) → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})))
67	66	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = ((iEdg‘𝑇)‘𝑥))
70	69	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗‘𝑦) = 𝑥 → (((iEdg‘𝑇)‘(𝑗‘𝑦)) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅}) ↔ ((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})))
71	68, 70	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . . . . . 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 48	. . . . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . . . 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 87	. . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . . . . . 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 3161	. . . . . . . . . . . . . . . . . . . 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 48	. . . . . . . . . . . . . . . . . . 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 3153	. . . . . . . . . . . . . . . . . 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 1137	. . . . . . . . . . . . . . . . 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 1137	. . . . . . . . . . . . . . . 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 99	. . . . . . . . . . . . . . 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 416	. . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . 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 412	. . . . . . . . . . . 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 7121	. . . . . . . . . . . 12 ⊢ (((iEdg‘𝑇) Fn dom (iEdg‘𝑇) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})) → ran (iEdg‘𝑇) ⊆ (𝒫 (Vtx‘𝑇) ∖ {∅}))
88	12, 86, 87	syl2an2r 698	. . . . . . . . . . 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 6727	. . . . . . . . . 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 418	. . . . . . . . 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 1137	. . . . . . . 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 1965	. . . . . . 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 412	. . . . . 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 18	. . . . 5 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (Fun (iEdg‘𝑇) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
95	94	impcom 413	. . . 4 ⊢ ((Fun (iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅})))
96		grimdmrel 49071	. . . . . . 7 ⊢ Rel dom GraphIso
97	96	ovrcl 7461	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
98	1, 3	isuhgr 29643	. . . . . . . 8 ⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
99	98	adantr 486	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
100	2, 4	isuhgr 29643	. . . . . . . 8 ⊢ (𝑇 ∈ V → (𝑇 ∈ UHGraph ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅})))
101	100	adantl 487	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑇 ∈ UHGraph ↔ (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅})))
102	99, 101	imbi12d 347	. . . . . 6 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
103	97, 102	syl 18	. . . . 5 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
104	103	adantl 487	. . . 4 ⊢ ((Fun (iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ((𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph) ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) → (iEdg‘𝑇):dom (iEdg‘𝑇)⟶(𝒫 (Vtx‘𝑇) ∖ {∅}))))
105	95, 104	mpbird 260	. . 3 ⊢ ((Fun (iEdg‘𝑇) ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → (𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph))
106	105	ex 418	. 2 ⊢ (Fun (iEdg‘𝑇) → (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ UHGraph → 𝑇 ∈ UHGraph)))
107	106	3imp31 1129	1 ⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇) ∧ Fun (iEdg‘𝑇)) → 𝑇 ∈ UHGraph)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∅c0 4278 𝒫 cpw 4556 {csn 4584 dom cdm 5650 ran crn 5651 “ cima 5653 Fun wfun 6532 Fn wfn 6533 ⟶wf 6534 –onto→wfo 6536 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 Vtxcvtx 29579 iEdgciedg 29580 UHGraphcuhgr 29639 GraphIso cgrim 49066

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-map 8852 df-uhgr 29641 df-grim 49069

This theorem is used by: (None)

W3C validator