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 48244

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 48240	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)–1-1-onto→dom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))))
6		fdmrn 6701	. . . . . . . . . . . . . 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 6530	. . . . . . . . . . . . . 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 6789	. . . . . . . . . . . . . . . . . . . . . . . 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 6903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗:dom (iEdg‘𝑆)–onto→dom (iEdg‘𝑇) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)
17	15, 16	sylan 581	. . . . . . . . . . . . . . . . . . . . 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 6847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑇)‘(𝑗‘𝑖)) = ((iEdg‘𝑇)‘(𝑗‘𝑦)))
20		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑆)‘𝑖) = ((iEdg‘𝑆)‘𝑦))
21	20	imaeq2d 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑦 → (𝐹 “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))
22	19, 21	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 = 𝑦 → (((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
23	22	rspcv 3574	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((Fun 𝐹 ∧ ((iEdg‘𝑆)‘𝑦) ∈ V) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) ∈ V)
31	27, 29, 30	syl2an2r 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) → 𝐹:(Vtx‘𝑆)⟶(Vtx‘𝑇))
33	32	fimassd 6691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 6786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝐹:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (dom 𝐹 ∩ ((iEdg‘𝑆)‘𝑦)) = ((Vtx‘𝑆) ∩ ((iEdg‘𝑆)‘𝑦)))
42		ffvelcdm 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
46	28	elpw 4560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆))
47	45, 46	bianbi 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((iEdg‘𝑆)‘𝑦) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ↔ (((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆) ∧ ((iEdg‘𝑆)‘𝑦) ≠ ∅))
48		sseqin2 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = ((iEdg‘𝑇)‘𝑥))
70	69	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3137	. . . . . . . . . . . . . . . . . . . 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 3129	. . . . . . . . . . . . . . . . . 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 7075	. . . . . . . . . . . 12 ⊢ (((iEdg‘𝑇) Fn dom (iEdg‘𝑇) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑇)‘𝑥) ∈ (𝒫 (Vtx‘𝑇) ∖ {∅})) → ran (iEdg‘𝑇) ⊆ (𝒫 (Vtx‘𝑇) ∖ {∅}))
88	12, 86, 87	syl2an2r 686	. . . . . . . . . . 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 6687	. . . . . . . . . 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 1935	. . . . . . 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 48237	. . . . . . 7 ⊢ Rel dom GraphIso
97	96	ovrcl 7409	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
98	1, 3	isuhgr 29145	. . . . . . . 8 ⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
99	98	adantr 480	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅})))
100	2, 4	isuhgr 29145	. . . . . . . 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 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ∖ cdif 3900 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 𝒫 cpw 4556 {csn 4582 dom cdm 5632 ran crn 5633 “ cima 5635 Fun wfun 6494 Fn wfn 6495 ⟶wf 6496 –onto→wfo 6498 –1-1-onto→wf1o 6499 ‘cfv 6500 (class class class)co 7368 Vtxcvtx 29081 iEdgciedg 29082 UHGraphcuhgr 29141 GraphIso cgrim 48232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-sbc 3743 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-map 8777 df-uhgr 29143 df-grim 48235

This theorem is referenced by: (None)

W3C validator