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

Theorem uspgrsprf1 42324
Description: The mapping 𝐹 is a one-to-one function from the "simple pseudographs" with a fixed set of vertices 𝑉 into the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 25-Nov-2021.)
Hypotheses
Ref Expression
uspgrsprf.p 𝑃 = 𝒫 (Pairs‘𝑉)
uspgrsprf.g 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}
uspgrsprf.f 𝐹 = (𝑔𝐺 ↦ (2nd𝑔))
Assertion
Ref Expression
uspgrsprf1 𝐹:𝐺1-1𝑃
Distinct variable groups:   𝑃,𝑒,𝑞,𝑣   𝑒,𝑉,𝑞,𝑣   𝑔,𝐺   𝑃,𝑔,𝑒,𝑣
Allowed substitution hints:   𝐹(𝑣,𝑒,𝑔,𝑞)   𝐺(𝑣,𝑒,𝑞)   𝑉(𝑔)

Proof of Theorem uspgrsprf1
Dummy variables 𝑎 𝑏 𝑓 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uspgrsprf.p . . 3 𝑃 = 𝒫 (Pairs‘𝑉)
2 uspgrsprf.g . . 3 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}
3 uspgrsprf.f . . 3 𝐹 = (𝑔𝐺 ↦ (2nd𝑔))
41, 2, 3uspgrsprf 42323 . 2 𝐹:𝐺𝑃
51, 2, 3uspgrsprfv 42322 . . . . 5 (𝑎𝐺 → (𝐹𝑎) = (2nd𝑎))
61, 2, 3uspgrsprfv 42322 . . . . 5 (𝑏𝐺 → (𝐹𝑏) = (2nd𝑏))
75, 6eqeqan12d 2829 . . . 4 ((𝑎𝐺𝑏𝐺) → ((𝐹𝑎) = (𝐹𝑏) ↔ (2nd𝑎) = (2nd𝑏)))
82eleq2i 2884 . . . . . 6 (𝑎𝐺𝑎 ∈ {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))})
9 elopab 5185 . . . . . 6 (𝑎 ∈ {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} ↔ ∃𝑣𝑒(𝑎 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))))
10 opeq12 4604 . . . . . . . . 9 ((𝑣 = 𝑤𝑒 = 𝑓) → ⟨𝑣, 𝑒⟩ = ⟨𝑤, 𝑓⟩)
1110eqeq2d 2823 . . . . . . . 8 ((𝑣 = 𝑤𝑒 = 𝑓) → (𝑎 = ⟨𝑣, 𝑒⟩ ↔ 𝑎 = ⟨𝑤, 𝑓⟩))
12 eqeq1 2817 . . . . . . . . . 10 (𝑣 = 𝑤 → (𝑣 = 𝑉𝑤 = 𝑉))
1312adantr 468 . . . . . . . . 9 ((𝑣 = 𝑤𝑒 = 𝑓) → (𝑣 = 𝑉𝑤 = 𝑉))
14 eqeq2 2824 . . . . . . . . . . 11 (𝑣 = 𝑤 → ((Vtx‘𝑞) = 𝑣 ↔ (Vtx‘𝑞) = 𝑤))
15 eqeq2 2824 . . . . . . . . . . 11 (𝑒 = 𝑓 → ((Edg‘𝑞) = 𝑒 ↔ (Edg‘𝑞) = 𝑓))
1614, 15bi2anan9 622 . . . . . . . . . 10 ((𝑣 = 𝑤𝑒 = 𝑓) → (((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒) ↔ ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))
1716rexbidv 3247 . . . . . . . . 9 ((𝑣 = 𝑤𝑒 = 𝑓) → (∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒) ↔ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))
1813, 17anbi12d 618 . . . . . . . 8 ((𝑣 = 𝑤𝑒 = 𝑓) → ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) ↔ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))))
1911, 18anbi12d 618 . . . . . . 7 ((𝑣 = 𝑤𝑒 = 𝑓) → ((𝑎 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ↔ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))))
2019cbvex2v 2457 . . . . . 6 (∃𝑣𝑒(𝑎 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ↔ ∃𝑤𝑓(𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))))
218, 9, 203bitri 288 . . . . 5 (𝑎𝐺 ↔ ∃𝑤𝑓(𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))))
222eleq2i 2884 . . . . . 6 (𝑏𝐺𝑏 ∈ {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))})
23 elopab 5185 . . . . . 6 (𝑏 ∈ {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} ↔ ∃𝑣𝑒(𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))))
2422, 23bitri 266 . . . . 5 (𝑏𝐺 ↔ ∃𝑣𝑒(𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))))
25 eqeq2 2824 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑉 → (𝑣 = 𝑤𝑣 = 𝑉))
26 opeq12 4604 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 𝑣𝑓 = 𝑒) → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)
2726ex 399 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑣 → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩))
2827equcoms 2117 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑤 → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩))
2925, 28syl6bir 245 . . . . . . . . . . . . . . 15 (𝑤 = 𝑉 → (𝑣 = 𝑉 → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
3029ad2antrl 710 . . . . . . . . . . . . . 14 ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑣 = 𝑉 → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
3130com12 32 . . . . . . . . . . . . 13 (𝑣 = 𝑉 → ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
3231ad2antrl 710 . . . . . . . . . . . 12 ((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
3332imp 395 . . . . . . . . . . 11 (((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (𝑓 = 𝑒 → ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩))
34 vex 3401 . . . . . . . . . . . . . 14 𝑤 ∈ V
35 vex 3401 . . . . . . . . . . . . . 14 𝑓 ∈ V
3634, 35op2ndd 7412 . . . . . . . . . . . . 13 (𝑎 = ⟨𝑤, 𝑓⟩ → (2nd𝑎) = 𝑓)
3736ad2antrl 710 . . . . . . . . . . . 12 (((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (2nd𝑎) = 𝑓)
38 vex 3401 . . . . . . . . . . . . . . 15 𝑣 ∈ V
39 vex 3401 . . . . . . . . . . . . . . 15 𝑒 ∈ V
4038, 39op2ndd 7412 . . . . . . . . . . . . . 14 (𝑏 = ⟨𝑣, 𝑒⟩ → (2nd𝑏) = 𝑒)
4140adantr 468 . . . . . . . . . . . . 13 ((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd𝑏) = 𝑒)
4241adantr 468 . . . . . . . . . . . 12 (((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (2nd𝑏) = 𝑒)
4337, 42eqeq12d 2828 . . . . . . . . . . 11 (((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → ((2nd𝑎) = (2nd𝑏) ↔ 𝑓 = 𝑒))
44 eqeq12 2826 . . . . . . . . . . . . . . . 16 ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ 𝑏 = ⟨𝑣, 𝑒⟩) → (𝑎 = 𝑏 ↔ ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩))
4544ex 399 . . . . . . . . . . . . . . 15 (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑏 = ⟨𝑣, 𝑒⟩ → (𝑎 = 𝑏 ↔ ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
4645adantr 468 . . . . . . . . . . . . . 14 ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑏 = ⟨𝑣, 𝑒⟩ → (𝑎 = 𝑏 ↔ ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
4746com12 32 . . . . . . . . . . . . 13 (𝑏 = ⟨𝑣, 𝑒⟩ → ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑎 = 𝑏 ↔ ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
4847adantr 468 . . . . . . . . . . . 12 ((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑎 = 𝑏 ↔ ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩)))
4948imp 395 . . . . . . . . . . 11 (((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (𝑎 = 𝑏 ↔ ⟨𝑤, 𝑓⟩ = ⟨𝑣, 𝑒⟩))
5033, 43, 493imtr4d 285 . . . . . . . . . 10 (((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏))
5150ex 399 . . . . . . . . 9 ((𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏)))
5251exlimivv 2023 . . . . . . . 8 (∃𝑣𝑒(𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏)))
5352com12 32 . . . . . . 7 ((𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (∃𝑣𝑒(𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏)))
5453exlimivv 2023 . . . . . 6 (∃𝑤𝑓(𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (∃𝑣𝑒(𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏)))
5554imp 395 . . . . 5 ((∃𝑤𝑓(𝑎 = ⟨𝑤, 𝑓⟩ ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) ∧ ∃𝑣𝑒(𝑏 = ⟨𝑣, 𝑒⟩ ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏))
5621, 24, 55syl2anb 587 . . . 4 ((𝑎𝐺𝑏𝐺) → ((2nd𝑎) = (2nd𝑏) → 𝑎 = 𝑏))
577, 56sylbid 231 . . 3 ((𝑎𝐺𝑏𝐺) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
5857rgen2a 3172 . 2 𝑎𝐺𝑏𝐺 ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏)
59 dff13 6739 . 2 (𝐹:𝐺1-1𝑃 ↔ (𝐹:𝐺𝑃 ∧ ∀𝑎𝐺𝑏𝐺 ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏)))
604, 58, 59mpbir2an 693 1 𝐹:𝐺1-1𝑃
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2157  wral 3103  wrex 3104  𝒫 cpw 4358  cop 4383  {copab 4913  cmpt 4930  wf 6100  1-1wf1 6101  cfv 6104  2nd c2nd 7400  Vtxcvtx 26094  Edgcedg 26159  USPGraphcuspgr 26264  Pairscspr 42296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-card 9051  df-cda 9278  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-nn 11309  df-2 11367  df-n0 11563  df-xnn0 11633  df-z 11647  df-uz 11908  df-fz 12553  df-hash 13341  df-edg 26160  df-upgr 26197  df-uspgr 26266  df-spr 42297
This theorem is referenced by:  uspgrsprf1o  42326
  Copyright terms: Public domain W3C validator