grimcnv - Mathbox for Alexander van der Vekens

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

Theorem grimcnv 49189

Description: The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.)

**Assertion**
Ref	Expression
grimcnv	⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ^◡𝐹 ∈ (𝑇 GraphIso 𝑆)))

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

Step	Hyp	Ref	Expression
1		eqid 2763	. . . . 5 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
2		eqid 2763	. . . . 5 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
3		eqid 2763	. . . . 5 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
4		eqid 2763	. . . . 5 ⊢ (iEdg‘𝑇) = (iEdg‘𝑇)
5	1, 2, 3, 4	grimprop 49184	. . . 4 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))))
6	5	adantl 487	. . 3 ⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))))
7		f1ocnv 6856	. . . . 5 ⊢ (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) → ^◡𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑆))
8	7	ad2antrl 741	. . . 4 ⊢ (((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))))) → ^◡𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑆))
9		vex 3458	. . . . . . . . 9 ⊢ 𝑗 ∈ V
10		cnvexg 7957	. . . . . . . . 9 ⊢ (𝑗 ∈ V → ^◡𝑗 ∈ V)
11	9, 10	mp1i 14	. . . . . . . 8 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → ^◡𝑗 ∈ V)
12		f1ocnv 6856	. . . . . . . . . 10 ⊢ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) → ^◡𝑗:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆))
13	12	ad2antrl 741	. . . . . . . . 9 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → ^◡𝑗:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆))
14		f1ofo 6851	. . . . . . . . . . . . 13 ⊢ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) → 𝑗:dom (iEdg‘𝑆)⟶ontodom (iEdg‘𝑇))
15	14	ad2antrl 741	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → 𝑗:dom (iEdg‘𝑆)⟶ontodom (iEdg‘𝑇))
16		foelcdmi 6966	. . . . . . . . . . . 12 ⊢ ((𝑗:dom (iEdg‘𝑆)⟶ontodom (iEdg‘𝑇) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)
17	15, 16	sylan 592	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥)
18		2fveq3 6910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑇)‘(𝑗‘𝑖)) = ((iEdg‘𝑇)‘(𝑗‘𝑦)))
19		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑦 → ((iEdg‘𝑆)‘𝑖) = ((iEdg‘𝑆)‘𝑦))
20	19	imaeq2d 6063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑦 → (𝐹 “ ((iEdg‘𝑆)‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))
21	18, 20	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑦 → (((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) ↔ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
22	21	rspcv 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ dom (iEdg‘𝑆) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
23	22	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
24		f1ocnvfv1 7304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (^◡𝑗‘(𝑗‘𝑦)) = 𝑦)
25	24	ad4ant23 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → (^◡𝑗‘(𝑗‘𝑦)) = 𝑦)
26	25	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = ((iEdg‘𝑆)‘𝑦))
27		f1of1 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) → 𝐹:(Vtx‘𝑆)⟶1-1(Vtx‘𝑇))
28	27	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → 𝐹:(Vtx‘𝑆)⟶1-1(Vtx‘𝑇))
29	1, 3	uhgrss 29669	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 ∈ UHGraph ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆))
30	29	ad5ant15 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆))
31		f1imacnv 6860	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:(Vtx‘𝑆)⟶1-1(Vtx‘𝑇) ∧ ((iEdg‘𝑆)‘𝑦) ⊆ (Vtx‘𝑆)) → (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))) = ((iEdg‘𝑆)‘𝑦))
32	28, 30, 31	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))) = ((iEdg‘𝑆)‘𝑦))
33	32	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑦) = (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
34	33	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑆)‘𝑦) = (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
35	26, 34	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
36	35	adantlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))))
37		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)))
38	37	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → (𝐹 “ ((iEdg‘𝑆)‘𝑦)) = ((iEdg‘𝑇)‘(𝑗‘𝑦)))
39	38	imaeq2d 6063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → (^◡𝐹 “ (𝐹 “ ((iEdg‘𝑆)‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))))
40	36, 39	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) ∧ (𝑗‘𝑦) ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))))
41	40	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) ∧ ((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦))) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦)))))
42	41	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (((iEdg‘𝑇)‘(𝑗‘𝑦)) = (𝐹 “ ((iEdg‘𝑆)‘𝑦)) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))))))
43	23, 42	syld 48	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))))))
44	43	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → (𝑦 ∈ dom (iEdg‘𝑆) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦)))))))
45	44	com23 87	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ 𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇)) → (∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)) → (𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦)))))))
46	45	impr 460	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → (𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))))))
47		eleq1 2852	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗‘𝑦) = 𝑥 → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) ↔ 𝑥 ∈ dom (iEdg‘𝑇)))
48		2fveq3 6910	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)))
49		fveq2 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑇)‘(𝑗‘𝑦)) = ((iEdg‘𝑇)‘𝑥))
50	49	imaeq2d 6063	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗‘𝑦) = 𝑥 → (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))
51	48, 50	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗‘𝑦) = 𝑥 → (((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))) ↔ ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
52	47, 51	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗‘𝑦) = 𝑥 → (((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦)))) ↔ (𝑥 ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))))
53	52	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ ((𝑗‘𝑦) = 𝑥 → ((𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘(𝑗‘𝑦))) = (^◡𝐹 “ ((iEdg‘𝑇)‘(𝑗‘𝑦))))) ↔ (𝑦 ∈ dom (iEdg‘𝑆) → (𝑥 ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))))
54	46, 53	syl5ibcom 248	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → ((𝑗‘𝑦) = 𝑥 → (𝑦 ∈ dom (iEdg‘𝑆) → (𝑥 ∈ dom (iEdg‘𝑇) → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))))
55	54	com24 96	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → (𝑥 ∈ dom (iEdg‘𝑇) → (𝑦 ∈ dom (iEdg‘𝑆) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))))
56	55	imp31 423	. . . . . . . . . . . 12 ⊢ ((((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) ∧ 𝑦 ∈ dom (iEdg‘𝑆)) → ((𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
57	56	rexlimdva 3167	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → (∃𝑦 ∈ dom (iEdg‘𝑆)(𝑗‘𝑦) = 𝑥 → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
58	17, 57	mpd 16	. . . . . . . . . 10 ⊢ (((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) ∧ 𝑥 ∈ dom (iEdg‘𝑇)) → ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))
59	58	ralrimiva 3158	. . . . . . . . 9 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))
60	13, 59	jca 521	. . . . . . . 8 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → (^◡𝑗:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
61		f1oeq1 6831	. . . . . . . . 9 ⊢ (𝑓 = ^◡𝑗 → (𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ↔ ^◡𝑗:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆)))
62		fveq1 6904	. . . . . . . . . . 11 ⊢ (𝑓 = ^◡𝑗 → (𝑓‘𝑥) = (^◡𝑗‘𝑥))
63	62	fveqeq2d 6913	. . . . . . . . . 10 ⊢ (𝑓 = ^◡𝑗 → (((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)) ↔ ((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
64	63	ralbidv 3189	. . . . . . . . 9 ⊢ (𝑓 = ^◡𝑗 → (∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)) ↔ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
65	61, 64	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = ^◡𝑗 → ((𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))) ↔ (^◡𝑗:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(^◡𝑗‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))))
66	11, 60, 65	spcedv 3556	. . . . . . 7 ⊢ ((((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) ∧ (𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖)))) → ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
67	66	ex 418	. . . . . 6 ⊢ (((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) → ((𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))))
68	67	exlimdv 1968	. . . . 5 ⊢ (((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ 𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇)) → (∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))) → ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥)))))
69	68	impr 460	. . . 4 ⊢ (((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))))) → ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))
70		grimdmrel 49181	. . . . . . . 8 ⊢ Rel dom GraphIso
71	70	ovrcl 7481	. . . . . . 7 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V))
72	71	simprd 501	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → 𝑇 ∈ V)
73	71	simpld 500	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → 𝑆 ∈ V)
74		cnvexg 7957	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → ^◡𝐹 ∈ V)
75	2, 1, 4, 3	isgrim 49183	. . . . . 6 ⊢ ((𝑇 ∈ V ∧ 𝑆 ∈ V ∧ ^◡𝐹 ∈ V) → (^◡𝐹 ∈ (𝑇 GraphIso 𝑆) ↔ (^◡𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑆) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))))
76	72, 73, 74, 75	syl3anc 1399	. . . . 5 ⊢ (𝐹 ∈ (𝑆 GraphIso 𝑇) → (^◡𝐹 ∈ (𝑇 GraphIso 𝑆) ↔ (^◡𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑆) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))))
77	76	ad2antlr 740	. . . 4 ⊢ (((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))))) → (^◡𝐹 ∈ (𝑇 GraphIso 𝑆) ↔ (^◡𝐹:(Vtx‘𝑇)⟶1-1onto(Vtx‘𝑆) ∧ ∃𝑓(𝑓:dom (iEdg‘𝑇)⟶1-1ontodom (iEdg‘𝑆) ∧ ∀𝑥 ∈ dom (iEdg‘𝑇)((iEdg‘𝑆)‘(𝑓‘𝑥)) = (^◡𝐹 “ ((iEdg‘𝑇)‘𝑥))))))
78	8, 69, 77	mpbir2and 726	. . 3 ⊢ (((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) ∧ (𝐹:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∃𝑗(𝑗:dom (iEdg‘𝑆)⟶1-1ontodom (iEdg‘𝑇) ∧ ∀𝑖 ∈ dom (iEdg‘𝑆)((iEdg‘𝑇)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝑆)‘𝑖))))) → ^◡𝐹 ∈ (𝑇 GraphIso 𝑆))
79	6, 78	mpdan 700	. 2 ⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇)) → ^◡𝐹 ∈ (𝑇 GraphIso 𝑆))
80	79	ex 418	1 ⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ^◡𝐹 ∈ (𝑇 GraphIso 𝑆)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ^◡ccnv 5654 dom cdm 5655 “ cima 5658 ⟶1-1wf1 6552 ⟶ontowfo 6553 ⟶1-1ontowf1o 6554 ‘cfv 6555 (class class class)co 7440 Vtxcvtx 29601 iEdgciedg 29602 UHGraphcuhgr 29661 GraphIso cgrim 49176

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-br 5107 df-opab 5171 df-mpt 5190 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-ov 7443 df-oprab 7444 df-mpo 7445 df-map 8874 df-uhgr 29663 df-grim 49179

This theorem is used by: uhgrimedg 49192 gricsym 49222

W3C validator