upgrimpths - Mathbox for Alexander van der Vekens

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

Theorem upgrimpths 48401

Description: Graph isomorphisms between simple pseudographs map paths onto paths. (Contributed by AV, 31-Oct-2025.)

**Hypotheses**
Ref	Expression
upgrimwlk.i	⊢ 𝐼 = (iEdg‘𝐺)
upgrimwlk.j	⊢ 𝐽 = (iEdg‘𝐻)
upgrimwlk.g	⊢ (𝜑 → 𝐺 ∈ USPGraph)
upgrimwlk.h	⊢ (𝜑 → 𝐻 ∈ USPGraph)
upgrimwlk.n	⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))
upgrimwlk.e	⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (^◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))
upgrimpths.p	⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)

**Assertion**
Ref	Expression
upgrimpths	⊢ (𝜑 → 𝐸(Paths‘𝐻)(𝑁 ∘ 𝑃))

Distinct variable groups: 𝑥,𝐹 𝑥,𝐺 𝑥,𝐼 𝑥,𝐽 𝑥,𝑃 𝜑,𝑥 𝑥,𝐸 𝑥,𝑁 Allowed substitution hint: 𝐻(𝑥)

Proof of Theorem upgrimpths Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		upgrimwlk.i	. . . 4 ⊢ 𝐼 = (iEdg‘𝐺)
2		upgrimwlk.j	. . . 4 ⊢ 𝐽 = (iEdg‘𝐻)
3		upgrimwlk.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ USPGraph)
4		upgrimwlk.h	. . . 4 ⊢ (𝜑 → 𝐻 ∈ USPGraph)
5		upgrimwlk.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))
6		upgrimwlk.e	. . . 4 ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (^◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))
7		upgrimpths.p	. . . . 5 ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
8		pthistrl 29810	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
9	7, 8	syl 17	. . . 4 ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
10	1, 2, 3, 4, 5, 6, 9	upgrimtrls 48398	. . 3 ⊢ (𝜑 → 𝐸(Trails‘𝐻)(𝑁 ∘ 𝑃))
11	1, 2, 3, 4, 5, 6, 7	upgrimpthslem1 48399	. . 3 ⊢ (𝜑 → Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))))
12		pthiswlk 29812	. . . . . . . . . . . 12 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
13	1	wlkf 29702	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
14	7, 12, 13	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
15		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
16	15	wlkp 29704	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))
17	7, 12, 16	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))
18	1, 2, 3, 4, 5, 6, 14, 17	upgrimwlklem4 48392	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 ∘ 𝑃):(0...(♯‘𝐸))⟶(Vtx‘𝐻))
19	18	ffnd 6665	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∘ 𝑃) Fn (0...(♯‘𝐸)))
20	1, 2, 3, 4, 5, 6, 14	upgrimwlklem1 48389	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐹))
21		wlkcl 29703	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ₀)
22	7, 12, 21	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ₀)
23	20, 22	eqeltrd 2837	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐸) ∈ ℕ₀)
24		0elfz 13573	. . . . . . . . . 10 ⊢ ((♯‘𝐸) ∈ ℕ₀ → 0 ∈ (0...(♯‘𝐸)))
25	23, 24	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...(♯‘𝐸)))
26		nn0fz0 13574	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) ∈ ℕ₀ ↔ (♯‘𝐹) ∈ (0...(♯‘𝐹)))
27	22, 26	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐹) ∈ (0...(♯‘𝐹)))
28	20	oveq2d 7378	. . . . . . . . . 10 ⊢ (𝜑 → (0...(♯‘𝐸)) = (0...(♯‘𝐹)))
29	27, 28	eleqtrrd 2840	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐹) ∈ (0...(♯‘𝐸)))
30		fnimapr 6919	. . . . . . . . 9 ⊢ (((𝑁 ∘ 𝑃) Fn (0...(♯‘𝐸)) ∧ 0 ∈ (0...(♯‘𝐸)) ∧ (♯‘𝐹) ∈ (0...(♯‘𝐸))) → ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) = {((𝑁 ∘ 𝑃)‘0), ((𝑁 ∘ 𝑃)‘(♯‘𝐹))})
31	19, 25, 29, 30	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) = {((𝑁 ∘ 𝑃)‘0), ((𝑁 ∘ 𝑃)‘(♯‘𝐹))})
32	31	eleq2d 2823	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ↔ 𝑥 ∈ {((𝑁 ∘ 𝑃)‘0), ((𝑁 ∘ 𝑃)‘(♯‘𝐹))}))
33		vex 3434	. . . . . . . 8 ⊢ 𝑥 ∈ V
34	33	elpr 4593	. . . . . . 7 ⊢ (𝑥 ∈ {((𝑁 ∘ 𝑃)‘0), ((𝑁 ∘ 𝑃)‘(♯‘𝐹))} ↔ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
35	32, 34	bitrdi 287	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ↔ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))))
36	1, 2, 3, 4, 5, 6, 7	upgrimpthslem2 48400	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → (¬ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘0) ∧ ¬ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
37	36	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘0))
38		eqeq2 2749	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝑁 ∘ 𝑃)‘0) → (((𝑁 ∘ 𝑃)‘𝑦) = 𝑥 ↔ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘0)))
39	38	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 ∘ 𝑃)‘0) → (¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥 ↔ ¬ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘0)))
40	37, 39	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → (𝑥 = ((𝑁 ∘ 𝑃)‘0) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥))
41	36	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))
42		eqeq2 2749	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)) → (((𝑁 ∘ 𝑃)‘𝑦) = 𝑥 ↔ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
43	42	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)) → (¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥 ↔ ¬ ((𝑁 ∘ 𝑃)‘𝑦) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
44	41, 43	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → (𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥))
45	40, 44	jaod 860	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → ((𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥))
46	45	impancom 451	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) → (𝑦 ∈ (1..^(♯‘𝐹)) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥))
47	46	imp 406	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) ∧ 𝑦 ∈ (1..^(♯‘𝐹))) → ¬ ((𝑁 ∘ 𝑃)‘𝑦) = 𝑥)
48	47	nrexdv 3133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) → ¬ ∃𝑦 ∈ (1..^(♯‘𝐹))((𝑁 ∘ 𝑃)‘𝑦) = 𝑥)
49	20	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐸))
50	49	oveq2d 7378	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...(♯‘𝐹)) = (0...(♯‘𝐸)))
51	50	feq2d 6648	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 ∘ 𝑃):(0...(♯‘𝐹))⟶(Vtx‘𝐻) ↔ (𝑁 ∘ 𝑃):(0...(♯‘𝐸))⟶(Vtx‘𝐻)))
52	18, 51	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ∘ 𝑃):(0...(♯‘𝐹))⟶(Vtx‘𝐻))
53	52	ffnd 6665	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 ∘ 𝑃) Fn (0...(♯‘𝐹)))
54	53	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) → (𝑁 ∘ 𝑃) Fn (0...(♯‘𝐹)))
55		fzo0ss1 13639	. . . . . . . . . . 11 ⊢ (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹))
56		fzossfz 13628	. . . . . . . . . . 11 ⊢ (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
57	55, 56	sstri 3932	. . . . . . . . . 10 ⊢ (1..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
58	57	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) → (1..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)))
59	54, 58	fvelimabd 6909	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) → (𝑥 ∈ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹))) ↔ ∃𝑦 ∈ (1..^(♯‘𝐹))((𝑁 ∘ 𝑃)‘𝑦) = 𝑥))
60	48, 59	mtbird 325	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹)))) → ¬ 𝑥 ∈ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹))))
61	60	ex 412	. . . . . 6 ⊢ (𝜑 → ((𝑥 = ((𝑁 ∘ 𝑃)‘0) ∨ 𝑥 = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))) → ¬ 𝑥 ∈ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))))
62	35, 61	sylbid 240	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) → ¬ 𝑥 ∈ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))))
63	62	ralrimiv 3129	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ¬ 𝑥 ∈ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹))))
64		disj 4391	. . . 4 ⊢ ((((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))) = ∅ ↔ ∀𝑥 ∈ ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ¬ 𝑥 ∈ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹))))
65	63, 64	sylibr 234	. . 3 ⊢ (𝜑 → (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))) = ∅)
66	20	oveq2d 7378	. . . . . . 7 ⊢ (𝜑 → (1..^(♯‘𝐸)) = (1..^(♯‘𝐹)))
67	66	reseq2d 5940	. . . . . 6 ⊢ (𝜑 → ((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐸))) = ((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))))
68	67	cnveqd 5826	. . . . 5 ⊢ (𝜑 → ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐸))) = ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))))
69	68	funeqd 6516	. . . 4 ⊢ (𝜑 → (Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐸))) ↔ Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹)))))
70		preq2 4679	. . . . . . . 8 ⊢ ((♯‘𝐸) = (♯‘𝐹) → {0, (♯‘𝐸)} = {0, (♯‘𝐹)})
71	70	imaeq2d 6021	. . . . . . 7 ⊢ ((♯‘𝐸) = (♯‘𝐹) → ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) = ((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}))
72		oveq2 7370	. . . . . . . 8 ⊢ ((♯‘𝐸) = (♯‘𝐹) → (1..^(♯‘𝐸)) = (1..^(♯‘𝐹)))
73	72	imaeq2d 6021	. . . . . . 7 ⊢ ((♯‘𝐸) = (♯‘𝐹) → ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸))) = ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹))))
74	71, 73	ineq12d 4162	. . . . . 6 ⊢ ((♯‘𝐸) = (♯‘𝐹) → (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸)))) = (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))))
75	74	eqeq1d 2739	. . . . 5 ⊢ ((♯‘𝐸) = (♯‘𝐹) → ((((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸)))) = ∅ ↔ (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))) = ∅))
76	20, 75	syl 17	. . . 4 ⊢ (𝜑 → ((((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸)))) = ∅ ↔ (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))) = ∅))
77	69, 76	3anbi23d 1442	. . 3 ⊢ (𝜑 → ((𝐸(Trails‘𝐻)(𝑁 ∘ 𝑃) ∧ Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐸))) ∧ (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸)))) = ∅) ↔ (𝐸(Trails‘𝐻)(𝑁 ∘ 𝑃) ∧ Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))) ∧ (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐹)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐹)))) = ∅)))
78	10, 11, 65, 77	mpbir3and 1344	. 2 ⊢ (𝜑 → (𝐸(Trails‘𝐻)(𝑁 ∘ 𝑃) ∧ Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐸))) ∧ (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸)))) = ∅))
79		ispth 29808	. 2 ⊢ (𝐸(Paths‘𝐻)(𝑁 ∘ 𝑃) ↔ (𝐸(Trails‘𝐻)(𝑁 ∘ 𝑃) ∧ Fun ^◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐸))) ∧ (((𝑁 ∘ 𝑃) “ {0, (♯‘𝐸)}) ∩ ((𝑁 ∘ 𝑃) “ (1..^(♯‘𝐸)))) = ∅))
80	78, 79	sylibr 234	1 ⊢ (𝜑 → 𝐸(Paths‘𝐻)(𝑁 ∘ 𝑃))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 {cpr 4570 class class class wbr 5086 ↦ cmpt 5167 ^◡ccnv 5625 dom cdm 5626 ↾ cres 5628 “ cima 5629 ∘ ccom 5630 Fun wfun 6488 Fn wfn 6489 ⟶wf 6490 ‘cfv 6494 (class class class)co 7362 0cc0 11033 1c1 11034 ℕ₀cn0 12432 ...cfz 13456 ..^cfzo 13603 ♯chash 14287 Word cword 14470 Vtxcvtx 29083 iEdgciedg 29084 USPGraphcuspgr 29235 Walkscwlks 29684 Trailsctrls 29776 Pathscpths 29797 GraphIso cgrim 48367

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 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ifp 1064 df-3or 1088 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-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-oadd 8404 df-er 8638 df-map 8770 df-pm 8771 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-dju 9820 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-2 12239 df-n0 12433 df-xnn0 12506 df-z 12520 df-uz 12784 df-fz 13457 df-fzo 13604 df-hash 14288 df-word 14471 df-edg 29135 df-uhgr 29145 df-upgr 29169 df-uspgr 29237 df-wlks 29687 df-trls 29778 df-pths 29801 df-grim 48370

This theorem is referenced by: upgrimcycls 48403

W3C validator