isomgreqve - Mathbox for Alexander van der Vekens

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

Theorem isomgreqve 47070

Description: A set is isomorphic to a hypergraph if it has the same vertices and the same edges. (Contributed by AV, 11-Nov-2022.)

**Assertion**
Ref	Expression
isomgreqve	⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → 𝐴 IsomGr 𝐵)

Proof of Theorem isomgreqve Dummy variables 𝑓 𝑔 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvexd 6900	. . . 4 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (Vtx‘𝐵) ∈ V)
2	1	resiexd 7213	. . 3 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ( I ↾ (Vtx‘𝐵)) ∈ V)
3		f1oi 6865	. . . . 5 ⊢ ( I ↾ (Vtx‘𝐵)):(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐵)
4		simprl 768	. . . . . 6 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (Vtx‘𝐴) = (Vtx‘𝐵))
5	4	f1oeq2d 6823	. . . . 5 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (( I ↾ (Vtx‘𝐵)):(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ↔ ( I ↾ (Vtx‘𝐵)):(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐵)))
6	3, 5	mpbiri 258	. . . 4 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ( I ↾ (Vtx‘𝐵)):(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵))
7		fvexd 6900	. . . . . . 7 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (iEdg‘𝐵) ∈ V)
8	7	dmexd 7893	. . . . . 6 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → dom (iEdg‘𝐵) ∈ V)
9	8	resiexd 7213	. . . . 5 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ( I ↾ dom (iEdg‘𝐵)) ∈ V)
10		f1oi 6865	. . . . . . 7 ⊢ ( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐵)
11		simprr 770	. . . . . . . . 9 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (iEdg‘𝐴) = (iEdg‘𝐵))
12	11	dmeqd 5899	. . . . . . . 8 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → dom (iEdg‘𝐴) = dom (iEdg‘𝐵))
13	12	f1oeq2d 6823	. . . . . . 7 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ ( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐵)))
14	10, 13	mpbiri 258	. . . . . 6 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
15		eqid 2726	. . . . . . . . . . . 12 ⊢ (Vtx‘𝐴) = (Vtx‘𝐴)
16		eqid 2726	. . . . . . . . . . . 12 ⊢ (iEdg‘𝐴) = (iEdg‘𝐴)
17	15, 16	uhgrss 28832	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ UHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐴))
18	17	ad4ant14 749	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐴))
19		sseq2 4003	. . . . . . . . . . . . 13 ⊢ ((Vtx‘𝐴) = (Vtx‘𝐵) → (((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐴) ↔ ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐵)))
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ (((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵)) → (((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐴) ↔ ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐵)))
21	20	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐴) ↔ ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐵)))
22	21	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐴) ↔ ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐵)))
23	18, 22	mpbid 231	. . . . . . . . 9 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐵))
24		resiima 6069	. . . . . . . . 9 ⊢ (((iEdg‘𝐴)‘𝑖) ⊆ (Vtx‘𝐵) → (( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐴)‘𝑖))
25	23, 24	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐴)‘𝑖))
26		fvresi 7167	. . . . . . . . . 10 ⊢ (𝑖 ∈ dom (iEdg‘𝐴) → (( I ↾ dom (iEdg‘𝐴))‘𝑖) = 𝑖)
27	26	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (( I ↾ dom (iEdg‘𝐴))‘𝑖) = 𝑖)
28	27	fveq2d 6889	. . . . . . . 8 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘(( I ↾ dom (iEdg‘𝐴))‘𝑖)) = ((iEdg‘𝐴)‘𝑖))
29		id 22	. . . . . . . . . . . 12 ⊢ ((iEdg‘𝐴) = (iEdg‘𝐵) → (iEdg‘𝐴) = (iEdg‘𝐵))
30		dmeq 5897	. . . . . . . . . . . . . 14 ⊢ ((iEdg‘𝐴) = (iEdg‘𝐵) → dom (iEdg‘𝐴) = dom (iEdg‘𝐵))
31	30	reseq2d 5975	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐴) = (iEdg‘𝐵) → ( I ↾ dom (iEdg‘𝐴)) = ( I ↾ dom (iEdg‘𝐵)))
32	31	fveq1d 6887	. . . . . . . . . . . 12 ⊢ ((iEdg‘𝐴) = (iEdg‘𝐵) → (( I ↾ dom (iEdg‘𝐴))‘𝑖) = (( I ↾ dom (iEdg‘𝐵))‘𝑖))
33	29, 32	fveq12d 6892	. . . . . . . . . . 11 ⊢ ((iEdg‘𝐴) = (iEdg‘𝐵) → ((iEdg‘𝐴)‘(( I ↾ dom (iEdg‘𝐴))‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
34	33	adantl 481	. . . . . . . . . 10 ⊢ (((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵)) → ((iEdg‘𝐴)‘(( I ↾ dom (iEdg‘𝐴))‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
35	34	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ((iEdg‘𝐴)‘(( I ↾ dom (iEdg‘𝐴))‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
36	35	adantr 480	. . . . . . . 8 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘(( I ↾ dom (iEdg‘𝐴))‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
37	25, 28, 36	3eqtr2d 2772	. . . . . . 7 ⊢ ((((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
38	37	ralrimiva 3140	. . . . . 6 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
39	14, 38	jca 511	. . . . 5 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖))))
40		f1oeq1 6815	. . . . . 6 ⊢ (𝑔 = ( I ↾ dom (iEdg‘𝐵)) → (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ ( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
41		fveq1 6884	. . . . . . . . 9 ⊢ (𝑔 = ( I ↾ dom (iEdg‘𝐵)) → (𝑔‘𝑖) = (( I ↾ dom (iEdg‘𝐵))‘𝑖))
42	41	fveq2d 6889	. . . . . . . 8 ⊢ (𝑔 = ( I ↾ dom (iEdg‘𝐵)) → ((iEdg‘𝐵)‘(𝑔‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))
43	42	eqeq2d 2737	. . . . . . 7 ⊢ (𝑔 = ( I ↾ dom (iEdg‘𝐵)) → ((( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) ↔ (( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖))))
44	43	ralbidv 3171	. . . . . 6 ⊢ (𝑔 = ( I ↾ dom (iEdg‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖))))
45	40, 44	anbi12d 630	. . . . 5 ⊢ (𝑔 = ( I ↾ dom (iEdg‘𝐵)) → ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ↔ (( I ↾ dom (iEdg‘𝐵)):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(( I ↾ dom (iEdg‘𝐵))‘𝑖)))))
46	9, 39, 45	spcedv 3582	. . . 4 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))
47	6, 46	jca 511	. . 3 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (( I ↾ (Vtx‘𝐵)):(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))))
48		f1oeq1 6815	. . . 4 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ↔ ( I ↾ (Vtx‘𝐵)):(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)))
49		imaeq1 6048	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)))
50	49	eqeq1d 2728	. . . . . . 7 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) ↔ (( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))
51	50	ralbidv 3171	. . . . . 6 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))
52	51	anbi2d 628	. . . . 5 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ↔ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))))
53	52	exbidv 1916	. . . 4 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → (∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))) ↔ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))))
54	48, 53	anbi12d 630	. . 3 ⊢ (𝑓 = ( I ↾ (Vtx‘𝐵)) → ((𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))) ↔ (( I ↾ (Vtx‘𝐵)):(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(( I ↾ (Vtx‘𝐵)) “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))))
55	2, 47, 54	spcedv 3582	. 2 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → ∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖)))))
56		eqid 2726	. . . 4 ⊢ (Vtx‘𝐵) = (Vtx‘𝐵)
57		eqid 2726	. . . 4 ⊢ (iEdg‘𝐵) = (iEdg‘𝐵)
58	15, 56, 16, 57	isomgr 47068	. . 3 ⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))))
59	58	adantr 480	. 2 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔‘𝑖))))))
60	55, 59	mpbird 257	1 ⊢ (((𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌) ∧ ((Vtx‘𝐴) = (Vtx‘𝐵) ∧ (iEdg‘𝐴) = (iEdg‘𝐵))) → 𝐴 IsomGr 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∀wral 3055 Vcvv 3468 ⊆ wss 3943 class class class wbr 5141 I cid 5566 dom cdm 5669 ↾ cres 5671 “ cima 5672 –1-1-onto→wf1o 6536 ‘cfv 6537 Vtxcvtx 28764 iEdgciedg 28765 UHGraphcuhgr 28824 IsomGr cisomgr 47064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pr 5420 ax-un 7722

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-ral 3056 df-rex 3065 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-uhgr 28826 df-isomgr 47066

This theorem is referenced by: isomgrref 47080 strisomgrop 47085

W3C validator