Theorem ushrisomgr 44026

Description: A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022.)

Hypotheses

Ref	Expression
ushrisomgr.v	⊢ 𝑉 = (Vtx‘𝐺)
ushrisomgr.e	⊢ 𝐸 = (Edg‘𝐺)
ushrisomgr.s	⊢ 𝐻 = ⟨𝑉, ( I ↾ 𝐸)⟩

Assertion

Ref	Expression
ushrisomgr	⊢ (𝐺 ∈ USHGraph → 𝐺 IsomGr 𝐻)

Proof of Theorem ushrisomgr

Dummy variables 𝑓 𝑔 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ushrisomgr.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
2	1	fvexi 6684	. . . . 5 ⊢ 𝑉 ∈ V
3	2	a1i 11	. . . 4 ⊢ (𝐺 ∈ USHGraph → 𝑉 ∈ V)
4	3	resiexd 6979	. . 3 ⊢ (𝐺 ∈ USHGraph → ( I ↾ 𝑉) ∈ V)
5		f1oi 6652	. . . . . 6 ⊢ ( I ↾ 𝑉):𝑉–1-1-onto→𝑉
6	5	a1i 11	. . . . 5 ⊢ (𝐺 ∈ USHGraph → ( I ↾ 𝑉):𝑉–1-1-onto→𝑉)
7		ushrisomgr.s	. . . . . . . 8 ⊢ 𝐻 = ⟨𝑉, ( I ↾ 𝐸)⟩
8	7	fveq2i 6673	. . . . . . 7 ⊢ (Vtx‘𝐻) = (Vtx‘⟨𝑉, ( I ↾ 𝐸)⟩)
9		ushrisomgr.e	. . . . . . . . . . 11 ⊢ 𝐸 = (Edg‘𝐺)
10	9	fvexi 6684	. . . . . . . . . 10 ⊢ 𝐸 ∈ V
11		id 22	. . . . . . . . . . 11 ⊢ (𝐸 ∈ V → 𝐸 ∈ V)
12	11	resiexd 6979	. . . . . . . . . 10 ⊢ (𝐸 ∈ V → ( I ↾ 𝐸) ∈ V)
13	10, 12	ax-mp 5	. . . . . . . . 9 ⊢ ( I ↾ 𝐸) ∈ V
14	2, 13	pm3.2i 473	. . . . . . . 8 ⊢ (𝑉 ∈ V ∧ ( I ↾ 𝐸) ∈ V)
15		opvtxfv 26789	. . . . . . . 8 ⊢ ((𝑉 ∈ V ∧ ( I ↾ 𝐸) ∈ V) → (Vtx‘⟨𝑉, ( I ↾ 𝐸)⟩) = 𝑉)
16	14, 15	mp1i 13	. . . . . . 7 ⊢ (𝐺 ∈ USHGraph → (Vtx‘⟨𝑉, ( I ↾ 𝐸)⟩) = 𝑉)
17	8, 16	syl5eq 2868	. . . . . 6 ⊢ (𝐺 ∈ USHGraph → (Vtx‘𝐻) = 𝑉)
18	17	f1oeq3d 6612	. . . . 5 ⊢ (𝐺 ∈ USHGraph → (( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻) ↔ ( I ↾ 𝑉):𝑉–1-1-onto→𝑉))
19	6, 18	mpbird 259	. . . 4 ⊢ (𝐺 ∈ USHGraph → ( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻))
20		fvexd 6685	. . . . 5 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐺) ∈ V)
21		eqid 2821	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
22	1, 21	ushgrf 26848	. . . . . . . 8 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 𝑉 ∖ {∅}))
23		f1f1orn 6626	. . . . . . . 8 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→ran (iEdg‘𝐺))
24	22, 23	syl 17	. . . . . . 7 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→ran (iEdg‘𝐺))
25	7	fveq2i 6673	. . . . . . . . . . 11 ⊢ (iEdg‘𝐻) = (iEdg‘⟨𝑉, ( I ↾ 𝐸)⟩)
26	10	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USHGraph → 𝐸 ∈ V)
27	26	resiexd 6979	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USHGraph → ( I ↾ 𝐸) ∈ V)
28		opiedgfv 26792	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ V ∧ ( I ↾ 𝐸) ∈ V) → (iEdg‘⟨𝑉, ( I ↾ 𝐸)⟩) = ( I ↾ 𝐸))
29	2, 27, 28	sylancr 589	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USHGraph → (iEdg‘⟨𝑉, ( I ↾ 𝐸)⟩) = ( I ↾ 𝐸))
30	25, 29	syl5eq 2868	. . . . . . . . . 10 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐻) = ( I ↾ 𝐸))
31	30	dmeqd 5774	. . . . . . . . 9 ⊢ (𝐺 ∈ USHGraph → dom (iEdg‘𝐻) = dom ( I ↾ 𝐸))
32		dmresi 5921	. . . . . . . . . 10 ⊢ dom ( I ↾ 𝐸) = 𝐸
33	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USHGraph → 𝐸 = (Edg‘𝐺))
34		edgval 26834	. . . . . . . . . . 11 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
35	33, 34	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝐺 ∈ USHGraph → 𝐸 = ran (iEdg‘𝐺))
36	32, 35	syl5eq 2868	. . . . . . . . 9 ⊢ (𝐺 ∈ USHGraph → dom ( I ↾ 𝐸) = ran (iEdg‘𝐺))
37	31, 36	eqtrd 2856	. . . . . . . 8 ⊢ (𝐺 ∈ USHGraph → dom (iEdg‘𝐻) = ran (iEdg‘𝐺))
38	37	f1oeq3d 6612	. . . . . . 7 ⊢ (𝐺 ∈ USHGraph → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→ran (iEdg‘𝐺)))
39	24, 38	mpbird 259	. . . . . 6 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
40		ushgruhgr 26854	. . . . . . . . . 10 ⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph)
41	1, 21	uhgrss 26849	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑉)
42	40, 41	sylan 582	. . . . . . . . 9 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑉)
43		resiima 5944	. . . . . . . . 9 ⊢ (((iEdg‘𝐺)‘𝑖) ⊆ 𝑉 → (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖))
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖))
45		f1f 6575	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
46	22, 45	syl 17	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅}))
47	46	ffund 6518	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USHGraph → Fun (iEdg‘𝐺))
48		fvelrn 6844	. . . . . . . . . . 11 ⊢ ((Fun (iEdg‘𝐺) ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ∈ ran (iEdg‘𝐺))
49	47, 48	sylan 582	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ∈ ran (iEdg‘𝐺))
50	9, 34	eqtri 2844	. . . . . . . . . 10 ⊢ 𝐸 = ran (iEdg‘𝐺)
51	49, 50	eleqtrrdi 2924	. . . . . . . . 9 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ∈ 𝐸)
52		fvresi 6935	. . . . . . . . 9 ⊢ (((iEdg‘𝐺)‘𝑖) ∈ 𝐸 → (( I ↾ 𝐸)‘((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖))
53	51, 52	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝐸)‘((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖))
54	10	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → 𝐸 ∈ V)
55	54	resiexd 6979	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ( I ↾ 𝐸) ∈ V)
56	2, 55, 28	sylancr 589	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (iEdg‘⟨𝑉, ( I ↾ 𝐸)⟩) = ( I ↾ 𝐸))
57	25, 56	syl5req 2869	. . . . . . . . 9 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ( I ↾ 𝐸) = (iEdg‘𝐻))
58	57	fveq1d 6672	. . . . . . . 8 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝐸)‘((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))
59	44, 53, 58	3eqtr2d 2862	. . . . . . 7 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))
60	59	ralrimiva 3182	. . . . . 6 ⊢ (𝐺 ∈ USHGraph → ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))
61	39, 60	jca 514	. . . . 5 ⊢ (𝐺 ∈ USHGraph → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))))
62		f1oeq1 6604	. . . . . 6 ⊢ (𝑔 = (iEdg‘𝐺) → (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)))
63		fveq1 6669	. . . . . . . . 9 ⊢ (𝑔 = (iEdg‘𝐺) → (𝑔‘𝑖) = ((iEdg‘𝐺)‘𝑖))
64	63	fveq2d 6674	. . . . . . . 8 ⊢ (𝑔 = (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))
65	64	eqeq2d 2832	. . . . . . 7 ⊢ (𝑔 = (iEdg‘𝐺) → ((( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))))
66	65	ralbidv 3197	. . . . . 6 ⊢ (𝑔 = (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))))
67	62, 66	anbi12d 632	. . . . 5 ⊢ (𝑔 = (iEdg‘𝐺) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) ↔ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))))
68	20, 61, 67	spcedv 3599	. . . 4 ⊢ (𝐺 ∈ USHGraph → ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))
69	19, 68	jca 514	. . 3 ⊢ (𝐺 ∈ USHGraph → (( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))
70		f1oeq1 6604	. . . 4 ⊢ (𝑓 = ( I ↾ 𝑉) → (𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ↔ ( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻)))
71		imaeq1 5924	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ 𝑉) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)))
72	71	eqeq1d 2823	. . . . . . 7 ⊢ (𝑓 = ( I ↾ 𝑉) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))
73	72	ralbidv 3197	. . . . . 6 ⊢ (𝑓 = ( I ↾ 𝑉) → (∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))
74	73	anbi2d 630	. . . . 5 ⊢ (𝑓 = ( I ↾ 𝑉) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) ↔ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))
75	74	exbidv 1922	. . . 4 ⊢ (𝑓 = ( I ↾ 𝑉) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) ↔ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))
76	70, 75	anbi12d 632	. . 3 ⊢ (𝑓 = ( I ↾ 𝑉) → ((𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))) ↔ (( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))))
77	4, 69, 76	spcedv 3599	. 2 ⊢ (𝐺 ∈ USHGraph → ∃𝑓(𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))
78		opex 5356	. . . 4 ⊢ ⟨𝑉, ( I ↾ 𝐸)⟩ ∈ V
79	7, 78	eqeltri 2909	. . 3 ⊢ 𝐻 ∈ V
80		eqid 2821	. . . 4 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
81		eqid 2821	. . . 4 ⊢ (iEdg‘𝐻) = (iEdg‘𝐻)
82	1, 80, 21, 81	isomgr 44008	. . 3 ⊢ ((𝐺 ∈ USHGraph ∧ 𝐻 ∈ V) → (𝐺 IsomGr 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))))
83	79, 82	mpan2 689	. 2 ⊢ (𝐺 ∈ USHGraph → (𝐺 IsomGr 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))))
84	77, 83	mpbird 259	1 ⊢ (𝐺 ∈ USHGraph → 𝐺 IsomGr 𝐻)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∀wral 3138  Vcvv 3494   ∖ cdif 3933   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  {csn 4567  ⟨cop 4573   class class class wbr 5066   I cid 5459  dom cdm 5555  ran crn 5556   ↾ cres 5557   “ cima 5558  Fun wfun 6349  ⟶wf 6351  –1-1→wf1 6352  –1-1-onto→wf1o 6354  ‘cfv 6355  Vtxcvtx 26781  iEdgciedg 26782  Edgcedg 26832  UHGraphcuhgr 26841  USHGraphcushgr 26842   IsomGr cisomgr 44004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-1st 7689  df-2nd 7690  df-vtx 26783  df-iedg 26784  df-edg 26833  df-uhgr 26843  df-ushgr 26844  df-isomgr 44006

This theorem is referenced by: (None)