Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brtrclfv2 Structured version   Visualization version   GIF version

Theorem brtrclfv2 39950
Description: Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.)
Assertion
Ref Expression
brtrclfv2 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑌 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
Distinct variable groups:   𝑅,𝑓   𝑈,𝑓   𝑓,𝑉   𝑓,𝑊   𝑓,𝑋   𝑓,𝑌

Proof of Theorem brtrclfv2
Dummy variables 𝑔 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 5058 . . . 4 (𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)})
21a1i 11 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}))
3 trclfv 14348 . . . . 5 (𝑅𝑊 → (t+‘𝑅) = {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)})
43breqd 5068 . . . 4 (𝑅𝑊 → (𝑋(t+‘𝑅)𝑌𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌))
543ad2ant3 1127 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌))
6 elimasng 5948 . . . 4 ((𝑋𝑈𝑌𝑉) → (𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}))
763adant3 1124 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}))
82, 5, 73bitr4d 312 . 2 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋})))
9 intimasn 39880 . . . . 5 (𝑋𝑈 → ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) = {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})})
1093ad2ant1 1125 . . . 4 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) = {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})})
11 simpl3 1185 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑅𝑊)
12 snex 5322 . . . . . . . . . . . . . . 15 {𝑋} ∈ V
13 vex 3495 . . . . . . . . . . . . . . 15 𝑓 ∈ V
1412, 13xpex 7465 . . . . . . . . . . . . . 14 ({𝑋} × 𝑓) ∈ V
15 unexg 7461 . . . . . . . . . . . . . 14 ((𝑅𝑊 ∧ ({𝑋} × 𝑓) ∈ V) → (𝑅 ∪ ({𝑋} × 𝑓)) ∈ V)
1611, 14, 15sylancl 586 . . . . . . . . . . . . 13 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (𝑅 ∪ ({𝑋} × 𝑓)) ∈ V)
17 trclfvlb 14356 . . . . . . . . . . . . . 14 ((𝑅 ∪ ({𝑋} × 𝑓)) ∈ V → (𝑅 ∪ ({𝑋} × 𝑓)) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
1817unssad 4160 . . . . . . . . . . . . 13 ((𝑅 ∪ ({𝑋} × 𝑓)) ∈ V → 𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
1916, 18syl 17 . . . . . . . . . . . 12 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
20 trclfvcotrg 14364 . . . . . . . . . . . . 13 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))
2120a1i 11 . . . . . . . . . . . 12 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
22 simpl1 1183 . . . . . . . . . . . . . . . . 17 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑋𝑈)
23 snidg 4589 . . . . . . . . . . . . . . . . 17 (𝑋𝑈𝑋 ∈ {𝑋})
2422, 23syl 17 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑋 ∈ {𝑋})
25 inelcm 4410 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ {𝑋} ∧ 𝑋 ∈ {𝑋}) → ({𝑋} ∩ {𝑋}) ≠ ∅)
2624, 24, 25syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ({𝑋} ∩ {𝑋}) ≠ ∅)
27 xpima2 6034 . . . . . . . . . . . . . . 15 (({𝑋} ∩ {𝑋}) ≠ ∅ → (({𝑋} × 𝑓) “ {𝑋}) = 𝑓)
2826, 27syl 17 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (({𝑋} × 𝑓) “ {𝑋}) = 𝑓)
2916, 17syl 17 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (𝑅 ∪ ({𝑋} × 𝑓)) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
3029unssbd 4161 . . . . . . . . . . . . . . 15 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ({𝑋} × 𝑓) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
31 imass1 5957 . . . . . . . . . . . . . . 15 (({𝑋} × 𝑓) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) → (({𝑋} × 𝑓) “ {𝑋}) ⊆ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
3230, 31syl 17 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (({𝑋} × 𝑓) “ {𝑋}) ⊆ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
3328, 32eqsstrrd 4003 . . . . . . . . . . . . 13 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑓 ⊆ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
34 imaundir 6002 . . . . . . . . . . . . . . 15 ((𝑅 ∪ ({𝑋} × 𝑓)) “ ({𝑋} ∪ 𝑓)) = ((𝑅 “ ({𝑋} ∪ 𝑓)) ∪ (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)))
35 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓)
36 imassrn 5933 . . . . . . . . . . . . . . . . . 18 (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)) ⊆ ran ({𝑋} × 𝑓)
37 rnxpss 6022 . . . . . . . . . . . . . . . . . 18 ran ({𝑋} × 𝑓) ⊆ 𝑓
3836, 37sstri 3973 . . . . . . . . . . . . . . . . 17 (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓
3938a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓)
4035, 39unssd 4159 . . . . . . . . . . . . . . 15 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ∪ (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓))) ⊆ 𝑓)
4134, 40eqsstrid 4012 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((𝑅 ∪ ({𝑋} × 𝑓)) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓)
42 trclimalb2 39949 . . . . . . . . . . . . . 14 (((𝑅 ∪ ({𝑋} × 𝑓)) ∈ V ∧ ((𝑅 ∪ ({𝑋} × 𝑓)) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}) ⊆ 𝑓)
4316, 41, 42syl2anc 584 . . . . . . . . . . . . 13 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}) ⊆ 𝑓)
4433, 43eqssd 3981 . . . . . . . . . . . 12 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑓 = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
45 sbcan 3818 . . . . . . . . . . . . 13 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})) ↔ ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ [(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋})))
46 sbcan 3818 . . . . . . . . . . . . . . 15 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ↔ ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟[(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟))
47 fvex 6676 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V
48 sbcssg 4459 . . . . . . . . . . . . . . . . . 18 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟))
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟)
50 csbconstg 3899 . . . . . . . . . . . . . . . . . . 19 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅 = 𝑅)
5147, 50ax-mp 5 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅 = 𝑅
5247csbvargi 4381 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))
5351, 52sseq12i 3994 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
5449, 53bitri 276 . . . . . . . . . . . . . . . 16 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
55 sbcssg 4459 . . . . . . . . . . . . . . . . . 18 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟))
5647, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟)
57 csbcog 39872 . . . . . . . . . . . . . . . . . . . 20 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟))
5847, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟)
5952, 52coeq12i 5727 . . . . . . . . . . . . . . . . . . 19 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
6058, 59eqtri 2841 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
6160, 52sseq12i 3994 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟 ↔ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
6256, 61bitri 276 . . . . . . . . . . . . . . . 16 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟 ↔ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
6354, 62anbi12i 626 . . . . . . . . . . . . . . 15 (([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟[(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟) ↔ (𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∧ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))))
6446, 63bitri 276 . . . . . . . . . . . . . 14 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ↔ (𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∧ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))))
65 sbceq2g 4365 . . . . . . . . . . . . . . . 16 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋}) ↔ 𝑓 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋})))
6647, 65ax-mp 5 . . . . . . . . . . . . . . 15 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋}) ↔ 𝑓 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}))
67 csbima12 5940 . . . . . . . . . . . . . . . . 17 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋})
6852imaeq1i 5919 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋})
69 csbconstg 3899 . . . . . . . . . . . . . . . . . . 19 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋} = {𝑋})
7047, 69ax-mp 5 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋} = {𝑋}
7170imaeq2i 5920 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋})
7267, 68, 713eqtri 2845 . . . . . . . . . . . . . . . 16 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋})
7372eqeq2i 2831 . . . . . . . . . . . . . . 15 (𝑓 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}) ↔ 𝑓 = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
7466, 73bitri 276 . . . . . . . . . . . . . 14 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋}) ↔ 𝑓 = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
7564, 74anbi12i 626 . . . . . . . . . . . . 13 (([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ [(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋})) ↔ ((𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∧ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ∧ 𝑓 = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋})))
7645, 75sylbbr 237 . . . . . . . . . . . 12 (((𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∧ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ∧ 𝑓 = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋})) → [(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
7719, 21, 44, 76syl21anc 833 . . . . . . . . . . 11 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → [(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
7877spesbcd 3863 . . . . . . . . . 10 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
7978ex 413 . . . . . . . . 9 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 → ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋}))))
80 eqeq1 2822 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (𝑔 = (𝑠 “ {𝑋}) ↔ 𝑓 = (𝑠 “ {𝑋})))
8180rexbidv 3294 . . . . . . . . . . 11 (𝑔 = 𝑓 → (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) ↔ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑓 = (𝑠 “ {𝑋})))
82 imaeq1 5917 . . . . . . . . . . . . 13 (𝑠 = 𝑟 → (𝑠 “ {𝑋}) = (𝑟 “ {𝑋}))
8382eqeq2d 2829 . . . . . . . . . . . 12 (𝑠 = 𝑟 → (𝑓 = (𝑠 “ {𝑋}) ↔ 𝑓 = (𝑟 “ {𝑋})))
8483rexab2 3688 . . . . . . . . . . 11 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑓 = (𝑠 “ {𝑋}) ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
8581, 84syl6bb 288 . . . . . . . . . 10 (𝑔 = 𝑓 → (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋}))))
8613, 85elab 3664 . . . . . . . . 9 (𝑓 ∈ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
8779, 86syl6ibr 253 . . . . . . . 8 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓𝑓 ∈ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})}))
88 intss1 4882 . . . . . . . 8 (𝑓 ∈ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} → {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓)
8987, 88syl6 35 . . . . . . 7 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓))
9089alrimiv 1919 . . . . . 6 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ∀𝑓((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓))
91 ssintab 4884 . . . . . 6 ( {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ↔ ∀𝑓((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓))
9290, 91sylibr 235 . . . . 5 ((𝑋𝑈𝑌𝑉𝑅𝑊) → {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
93 ssintab 4884 . . . . . . 7 ( {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ↔ ∀𝑔(∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ 𝑔))
9482eqeq2d 2829 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝑔 = (𝑠 “ {𝑋}) ↔ 𝑔 = (𝑟 “ {𝑋})))
9594rexab2 3688 . . . . . . . . 9 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})))
96 simpr 485 . . . . . . . . . . 11 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → 𝑔 = (𝑟 “ {𝑋}))
97 imass1 5957 . . . . . . . . . . . . . . 15 (𝑅𝑟 → (𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}))
9897adantr 481 . . . . . . . . . . . . . 14 ((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) → (𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}))
99 imass1 5957 . . . . . . . . . . . . . . 15 (𝑅𝑟 → (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ (𝑟 “ {𝑋})))
100 imaco 6097 . . . . . . . . . . . . . . . 16 ((𝑟𝑟) “ {𝑋}) = (𝑟 “ (𝑟 “ {𝑋}))
101 imass1 5957 . . . . . . . . . . . . . . . 16 ((𝑟𝑟) ⊆ 𝑟 → ((𝑟𝑟) “ {𝑋}) ⊆ (𝑟 “ {𝑋}))
102100, 101eqsstrrid 4013 . . . . . . . . . . . . . . 15 ((𝑟𝑟) ⊆ 𝑟 → (𝑟 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))
10399, 102sylan9ss 3977 . . . . . . . . . . . . . 14 ((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) → (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))
10498, 103jca 512 . . . . . . . . . . . . 13 ((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) → ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
105104adantr 481 . . . . . . . . . . . 12 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
106 vex 3495 . . . . . . . . . . . . . 14 𝑟 ∈ V
107106imaex 7610 . . . . . . . . . . . . 13 (𝑟 “ {𝑋}) ∈ V
108 imaundi 6001 . . . . . . . . . . . . . . . 16 (𝑅 “ ({𝑋} ∪ 𝑓)) = ((𝑅 “ {𝑋}) ∪ (𝑅𝑓))
109108sseq1i 3992 . . . . . . . . . . . . . . 15 ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 ↔ ((𝑅 “ {𝑋}) ∪ (𝑅𝑓)) ⊆ 𝑓)
110 unss 4157 . . . . . . . . . . . . . . 15 (((𝑅 “ {𝑋}) ⊆ 𝑓 ∧ (𝑅𝑓) ⊆ 𝑓) ↔ ((𝑅 “ {𝑋}) ∪ (𝑅𝑓)) ⊆ 𝑓)
111109, 110bitr4i 279 . . . . . . . . . . . . . 14 ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 ↔ ((𝑅 “ {𝑋}) ⊆ 𝑓 ∧ (𝑅𝑓) ⊆ 𝑓))
112 imaeq2 5918 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑟 “ {𝑋}) → (𝑅𝑓) = (𝑅 “ (𝑟 “ {𝑋})))
113 id 22 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑟 “ {𝑋}) → 𝑓 = (𝑟 “ {𝑋}))
114112, 113sseq12d 3997 . . . . . . . . . . . . . . 15 (𝑓 = (𝑟 “ {𝑋}) → ((𝑅𝑓) ⊆ 𝑓 ↔ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
115114cleq2lem 39846 . . . . . . . . . . . . . 14 (𝑓 = (𝑟 “ {𝑋}) → (((𝑅 “ {𝑋}) ⊆ 𝑓 ∧ (𝑅𝑓) ⊆ 𝑓) ↔ ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))))
116111, 115syl5bb 284 . . . . . . . . . . . . 13 (𝑓 = (𝑟 “ {𝑋}) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 ↔ ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))))
117107, 116elab 3664 . . . . . . . . . . . 12 ((𝑟 “ {𝑋}) ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ↔ ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
118105, 117sylibr 235 . . . . . . . . . . 11 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → (𝑟 “ {𝑋}) ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
11996, 118eqeltrd 2910 . . . . . . . . . 10 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → 𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
120119exlimiv 1922 . . . . . . . . 9 (∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → 𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
12195, 120sylbi 218 . . . . . . . 8 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) → 𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
122 intss1 4882 . . . . . . . 8 (𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ 𝑔)
123121, 122syl 17 . . . . . . 7 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ 𝑔)
12493, 123mpgbir 1791 . . . . . 6 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})}
125124a1i 11 . . . . 5 ((𝑋𝑈𝑌𝑉𝑅𝑊) → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})})
12692, 125eqssd 3981 . . . 4 ((𝑋𝑈𝑌𝑉𝑅𝑊) → {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} = {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
12710, 126eqtrd 2853 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) = {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
128127eleq2d 2895 . 2 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) ↔ 𝑌 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
1298, 128bitrd 280 1 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑌 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079  wal 1526   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  wrex 3136  Vcvv 3492  [wsbc 3769  csb 3880  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557  cop 4563   cint 4867   class class class wbr 5057   × cxp 5546  ran crn 5549  cima 5551  ccom 5552  cfv 6348  t+ctcl 14333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-seq 13358  df-trcl 14335  df-relexp 14368
This theorem is referenced by:  dffrege76  40163
  Copyright terms: Public domain W3C validator