Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mrsubrn Structured version   Visualization version   GIF version

Theorem mrsubrn 31749
Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mrsubvr.v 𝑉 = (mVR‘𝑇)
mrsubvr.r 𝑅 = (mREx‘𝑇)
mrsubvr.s 𝑆 = (mRSubst‘𝑇)
Assertion
Ref Expression
mrsubrn ran 𝑆 = (𝑆 “ (𝑅𝑚 𝑉))

Proof of Theorem mrsubrn
Dummy variables 𝑒 𝑓 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mrsubvr.v . . . . . . 7 𝑉 = (mVR‘𝑇)
2 mrsubvr.r . . . . . . 7 𝑅 = (mREx‘𝑇)
3 mrsubvr.s . . . . . . 7 𝑆 = (mRSubst‘𝑇)
41, 2, 3mrsubff 31748 . . . . . 6 (𝑇 ∈ V → 𝑆:(𝑅pm 𝑉)⟶(𝑅𝑚 𝑅))
5 ffn 6186 . . . . . 6 (𝑆:(𝑅pm 𝑉)⟶(𝑅𝑚 𝑅) → 𝑆 Fn (𝑅pm 𝑉))
64, 5syl 17 . . . . 5 (𝑇 ∈ V → 𝑆 Fn (𝑅pm 𝑉))
7 eleq1w 2833 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝑥 ∈ dom 𝑓𝑣 ∈ dom 𝑓))
8 fveq2 6333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → (𝑓𝑥) = (𝑓𝑣))
9 s1eq 13581 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑣 → ⟨“𝑥”⟩ = ⟨“𝑣”⟩)
107, 8, 9ifbieq12d 4253 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩) = if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
11 eqid 2771 . . . . . . . . . . . . . . . . 17 (𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)) = (𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))
12 fvex 6343 . . . . . . . . . . . . . . . . . 18 (𝑓𝑣) ∈ V
13 s1cli 13586 . . . . . . . . . . . . . . . . . . 19 ⟨“𝑣”⟩ ∈ Word V
1413elexi 3365 . . . . . . . . . . . . . . . . . 18 ⟨“𝑣”⟩ ∈ V
1512, 14ifex 4296 . . . . . . . . . . . . . . . . 17 if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩) ∈ V
1610, 11, 15fvmpt 6425 . . . . . . . . . . . . . . . 16 (𝑣𝑉 → ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣) = if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
1716adantl 467 . . . . . . . . . . . . . . 15 (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑣𝑉) → ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣) = if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
1817ifeq1da 4256 . . . . . . . . . . . . . 14 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩) = if(𝑣𝑉, if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩), ⟨“𝑣”⟩))
19 ifan 4274 . . . . . . . . . . . . . 14 if((𝑣𝑉𝑣 ∈ dom 𝑓), (𝑓𝑣), ⟨“𝑣”⟩) = if(𝑣𝑉, if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩), ⟨“𝑣”⟩)
2018, 19syl6eqr 2823 . . . . . . . . . . . . 13 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩) = if((𝑣𝑉𝑣 ∈ dom 𝑓), (𝑓𝑣), ⟨“𝑣”⟩))
21 elpmi 8029 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (𝑅pm 𝑉) → (𝑓:dom 𝑓𝑅 ∧ dom 𝑓𝑉))
2221adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑓:dom 𝑓𝑅 ∧ dom 𝑓𝑉))
2322simprd 479 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → dom 𝑓𝑉)
2423sseld 3752 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑣 ∈ dom 𝑓𝑣𝑉))
2524pm4.71rd 546 . . . . . . . . . . . . . . 15 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑣 ∈ dom 𝑓 ↔ (𝑣𝑉𝑣 ∈ dom 𝑓)))
2625bicomd 213 . . . . . . . . . . . . . 14 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → ((𝑣𝑉𝑣 ∈ dom 𝑓) ↔ 𝑣 ∈ dom 𝑓))
2726ifbid 4248 . . . . . . . . . . . . 13 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → if((𝑣𝑉𝑣 ∈ dom 𝑓), (𝑓𝑣), ⟨“𝑣”⟩) = if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩))
2820, 27eqtr2d 2806 . . . . . . . . . . . 12 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩) = if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩))
2928mpteq2dv 4880 . . . . . . . . . . 11 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩)))
3029coeq1d 5423 . . . . . . . . . 10 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒) = ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
3130oveq2d 6810 . . . . . . . . 9 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)) = ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
3231mpteq2dv 4880 . . . . . . . 8 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑒𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = (𝑒𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
33 eqid 2771 . . . . . . . . . 10 (mCN‘𝑇) = (mCN‘𝑇)
34 eqid 2771 . . . . . . . . . 10 (freeMnd‘((mCN‘𝑇) ∪ 𝑉)) = (freeMnd‘((mCN‘𝑇) ∪ 𝑉))
3533, 1, 2, 3, 34mrsubfval 31744 . . . . . . . . 9 ((𝑓:dom 𝑓𝑅 ∧ dom 𝑓𝑉) → (𝑆𝑓) = (𝑒𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
3622, 35syl 17 . . . . . . . 8 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑆𝑓) = (𝑒𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
3722simpld 478 . . . . . . . . . . . . 13 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → 𝑓:dom 𝑓𝑅)
3837adantr 466 . . . . . . . . . . . 12 (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) → 𝑓:dom 𝑓𝑅)
3938ffvelrnda 6503 . . . . . . . . . . 11 ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ 𝑅)
40 elun2 3933 . . . . . . . . . . . . . 14 (𝑥𝑉𝑥 ∈ ((mCN‘𝑇) ∪ 𝑉))
4140ad2antlr 700 . . . . . . . . . . . . 13 ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 𝑥 ∈ ((mCN‘𝑇) ∪ 𝑉))
4241s1cld 13584 . . . . . . . . . . . 12 ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → ⟨“𝑥”⟩ ∈ Word ((mCN‘𝑇) ∪ 𝑉))
4333, 1, 2mrexval 31737 . . . . . . . . . . . . 13 (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
4443ad3antrrr 703 . . . . . . . . . . . 12 ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉))
4542, 44eleqtrrd 2853 . . . . . . . . . . 11 ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → ⟨“𝑥”⟩ ∈ 𝑅)
4639, 45ifclda 4260 . . . . . . . . . 10 (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) ∧ 𝑥𝑉) → if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩) ∈ 𝑅)
4746, 11fmptd 6528 . . . . . . . . 9 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)):𝑉𝑅)
48 ssid 3774 . . . . . . . . 9 𝑉𝑉
4933, 1, 2, 3, 34mrsubfval 31744 . . . . . . . . 9 (((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)):𝑉𝑅𝑉𝑉) → (𝑆‘(𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))) = (𝑒𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
5047, 48, 49sylancl 568 . . . . . . . 8 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑆‘(𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))) = (𝑒𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣𝑉, ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))‘𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
5132, 36, 503eqtr4d 2815 . . . . . . 7 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑆𝑓) = (𝑆‘(𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))))
526adantr 466 . . . . . . . 8 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → 𝑆 Fn (𝑅pm 𝑉))
53 mapsspm 8044 . . . . . . . . 9 (𝑅𝑚 𝑉) ⊆ (𝑅pm 𝑉)
5453a1i 11 . . . . . . . 8 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑅𝑚 𝑉) ⊆ (𝑅pm 𝑉))
55 fvex 6343 . . . . . . . . . . 11 (mREx‘𝑇) ∈ V
562, 55eqeltri 2846 . . . . . . . . . 10 𝑅 ∈ V
57 fvex 6343 . . . . . . . . . . 11 (mVR‘𝑇) ∈ V
581, 57eqeltri 2846 . . . . . . . . . 10 𝑉 ∈ V
5956, 58elmap 8039 . . . . . . . . 9 ((𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)) ∈ (𝑅𝑚 𝑉) ↔ (𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)):𝑉𝑅)
6047, 59sylibr 224 . . . . . . . 8 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)) ∈ (𝑅𝑚 𝑉))
61 fnfvima 6640 . . . . . . . 8 ((𝑆 Fn (𝑅pm 𝑉) ∧ (𝑅𝑚 𝑉) ⊆ (𝑅pm 𝑉) ∧ (𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩)) ∈ (𝑅𝑚 𝑉)) → (𝑆‘(𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))) ∈ (𝑆 “ (𝑅𝑚 𝑉)))
6252, 54, 60, 61syl3anc 1476 . . . . . . 7 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑆‘(𝑥𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓𝑥), ⟨“𝑥”⟩))) ∈ (𝑆 “ (𝑅𝑚 𝑉)))
6351, 62eqeltrd 2850 . . . . . 6 ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅pm 𝑉)) → (𝑆𝑓) ∈ (𝑆 “ (𝑅𝑚 𝑉)))
6463ralrimiva 3115 . . . . 5 (𝑇 ∈ V → ∀𝑓 ∈ (𝑅pm 𝑉)(𝑆𝑓) ∈ (𝑆 “ (𝑅𝑚 𝑉)))
65 ffnfv 6531 . . . . 5 (𝑆:(𝑅pm 𝑉)⟶(𝑆 “ (𝑅𝑚 𝑉)) ↔ (𝑆 Fn (𝑅pm 𝑉) ∧ ∀𝑓 ∈ (𝑅pm 𝑉)(𝑆𝑓) ∈ (𝑆 “ (𝑅𝑚 𝑉))))
666, 64, 65sylanbrc 566 . . . 4 (𝑇 ∈ V → 𝑆:(𝑅pm 𝑉)⟶(𝑆 “ (𝑅𝑚 𝑉)))
67 frn 6194 . . . 4 (𝑆:(𝑅pm 𝑉)⟶(𝑆 “ (𝑅𝑚 𝑉)) → ran 𝑆 ⊆ (𝑆 “ (𝑅𝑚 𝑉)))
6866, 67syl 17 . . 3 (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅𝑚 𝑉)))
69 fvprc 6327 . . . . . . 7 𝑇 ∈ V → (mRSubst‘𝑇) = ∅)
703, 69syl5eq 2817 . . . . . 6 𝑇 ∈ V → 𝑆 = ∅)
7170rneqd 5492 . . . . 5 𝑇 ∈ V → ran 𝑆 = ran ∅)
72 rn0 5516 . . . . 5 ran ∅ = ∅
7371, 72syl6eq 2821 . . . 4 𝑇 ∈ V → ran 𝑆 = ∅)
74 0ss 4117 . . . 4 ∅ ⊆ (𝑆 “ (𝑅𝑚 𝑉))
7573, 74syl6eqss 3805 . . 3 𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅𝑚 𝑉)))
7668, 75pm2.61i 176 . 2 ran 𝑆 ⊆ (𝑆 “ (𝑅𝑚 𝑉))
77 imassrn 5619 . 2 (𝑆 “ (𝑅𝑚 𝑉)) ⊆ ran 𝑆
7876, 77eqssi 3769 1 ran 𝑆 = (𝑆 “ (𝑅𝑚 𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 382   = wceq 1631  wcel 2145  wral 3061  Vcvv 3351  cun 3722  wss 3724  c0 4064  ifcif 4226  cmpt 4864  dom cdm 5250  ran crn 5251  cima 5253  ccom 5254   Fn wfn 6027  wf 6028  cfv 6032  (class class class)co 6794  𝑚 cmap 8010  pm cpm 8011  Word cword 13488  ⟨“cs1 13491   Σg cgsu 16310  freeMndcfrmd 17593  mCNcmcn 31696  mVRcmvar 31697  mRExcmrex 31702  mRSubstcmrsub 31706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-map 8012  df-pm 8013  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-card 8966  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-nn 11224  df-2 11282  df-n0 11496  df-z 11581  df-uz 11890  df-fz 12535  df-fzo 12675  df-seq 13010  df-hash 13323  df-word 13496  df-concat 13498  df-s1 13499  df-struct 16067  df-ndx 16068  df-slot 16069  df-base 16071  df-sets 16072  df-ress 16073  df-plusg 16163  df-0g 16311  df-gsum 16312  df-mgm 17451  df-sgrp 17493  df-mnd 17504  df-submnd 17545  df-frmd 17595  df-mrex 31722  df-mrsub 31726
This theorem is referenced by:  mrsubff1o  31751  mrsub0  31752  mrsubccat  31754  mrsubcn  31755  msubrn  31765
  Copyright terms: Public domain W3C validator