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 39940
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 5064 . . . 4 (𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)})
21a1i 11 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}))
3 trclfv 14350 . . . . 5 (𝑅𝑊 → (t+‘𝑅) = {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)})
43breqd 5074 . . . 4 (𝑅𝑊 → (𝑋(t+‘𝑅)𝑌𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌))
543ad2ant3 1129 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑋 {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑌))
6 elimasng 5953 . . . 4 ((𝑋𝑈𝑌𝑉) → (𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}))
763adant3 1126 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) ↔ ⟨𝑋, 𝑌⟩ ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}))
82, 5, 73bitr4d 312 . 2 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋})))
9 intimasn 39870 . . . . 5 (𝑋𝑈 → ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) = {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})})
1093ad2ant1 1127 . . . 4 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) = {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})})
11 simpl3 1187 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑅𝑊)
12 snex 5328 . . . . . . . . . . . . . . 15 {𝑋} ∈ V
13 vex 3503 . . . . . . . . . . . . . . 15 𝑓 ∈ V
1412, 13xpex 7465 . . . . . . . . . . . . . 14 ({𝑋} × 𝑓) ∈ V
15 unexg 7461 . . . . . . . . . . . . . 14 ((𝑅𝑊 ∧ ({𝑋} × 𝑓) ∈ V) → (𝑅 ∪ ({𝑋} × 𝑓)) ∈ V)
1611, 14, 15sylancl 586 . . . . . . . . . . . . 13 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (𝑅 ∪ ({𝑋} × 𝑓)) ∈ V)
17 trclfvlb 14358 . . . . . . . . . . . . . 14 ((𝑅 ∪ ({𝑋} × 𝑓)) ∈ V → (𝑅 ∪ ({𝑋} × 𝑓)) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
1817unssad 4167 . . . . . . . . . . . . 13 ((𝑅 ∪ ({𝑋} × 𝑓)) ∈ V → 𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
1916, 18syl 17 . . . . . . . . . . . 12 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
20 trclfvcotrg 14366 . . . . . . . . . . . . 13 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))
2120a1i 11 . . . . . . . . . . . 12 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
22 simpl1 1185 . . . . . . . . . . . . . . . . 17 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑋𝑈)
23 snidg 4596 . . . . . . . . . . . . . . . . 17 (𝑋𝑈𝑋 ∈ {𝑋})
2422, 23syl 17 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑋 ∈ {𝑋})
25 inelcm 4417 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ {𝑋} ∧ 𝑋 ∈ {𝑋}) → ({𝑋} ∩ {𝑋}) ≠ ∅)
2624, 24, 25syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ({𝑋} ∩ {𝑋}) ≠ ∅)
27 xpima2 6039 . . . . . . . . . . . . . . 15 (({𝑋} ∩ {𝑋}) ≠ ∅ → (({𝑋} × 𝑓) “ {𝑋}) = 𝑓)
2826, 27syl 17 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (({𝑋} × 𝑓) “ {𝑋}) = 𝑓)
2916, 17syl 17 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (𝑅 ∪ ({𝑋} × 𝑓)) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
3029unssbd 4168 . . . . . . . . . . . . . . 15 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ({𝑋} × 𝑓) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
31 imass1 5962 . . . . . . . . . . . . . . 15 (({𝑋} × 𝑓) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) → (({𝑋} × 𝑓) “ {𝑋}) ⊆ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
3230, 31syl 17 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (({𝑋} × 𝑓) “ {𝑋}) ⊆ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
3328, 32eqsstrrd 4010 . . . . . . . . . . . . 13 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑓 ⊆ ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
34 imaundir 6007 . . . . . . . . . . . . . . 15 ((𝑅 ∪ ({𝑋} × 𝑓)) “ ({𝑋} ∪ 𝑓)) = ((𝑅 “ ({𝑋} ∪ 𝑓)) ∪ (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)))
35 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓)
36 imassrn 5938 . . . . . . . . . . . . . . . . . 18 (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)) ⊆ ran ({𝑋} × 𝑓)
37 rnxpss 6027 . . . . . . . . . . . . . . . . . 18 ran ({𝑋} × 𝑓) ⊆ 𝑓
3836, 37sstri 3980 . . . . . . . . . . . . . . . . 17 (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓
3938a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓)
4035, 39unssd 4166 . . . . . . . . . . . . . . 15 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ∪ (({𝑋} × 𝑓) “ ({𝑋} ∪ 𝑓))) ⊆ 𝑓)
4134, 40eqsstrid 4019 . . . . . . . . . . . . . 14 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((𝑅 ∪ ({𝑋} × 𝑓)) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓)
42 trclimalb2 39939 . . . . . . . . . . . . . 14 (((𝑅 ∪ ({𝑋} × 𝑓)) ∈ V ∧ ((𝑅 ∪ ({𝑋} × 𝑓)) “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}) ⊆ 𝑓)
4316, 41, 42syl2anc 584 . . . . . . . . . . . . 13 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}) ⊆ 𝑓)
4433, 43eqssd 3988 . . . . . . . . . . . 12 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → 𝑓 = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋}))
45 sbcan 3825 . . . . . . . . . . . . 13 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})) ↔ ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ [(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋})))
46 sbcan 3825 . . . . . . . . . . . . . . 15 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ↔ ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟[(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟))
47 fvex 6680 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V
48 sbcssg 4466 . . . . . . . . . . . . . . . . . 18 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟))
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟)
50 csbconstg 3906 . . . . . . . . . . . . . . . . . . 19 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅 = 𝑅)
5147, 50ax-mp 5 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅 = 𝑅
5247csbvargi 4388 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓)))
5351, 52sseq12i 4001 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑅(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
5449, 53bitri 276 . . . . . . . . . . . . . . . 16 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑅𝑟𝑅 ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
55 sbcssg 4466 . . . . . . . . . . . . . . . . . 18 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟))
5647, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟](𝑟𝑟) ⊆ 𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) ⊆ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟)
57 csbcog 39862 . . . . . . . . . . . . . . . . . . . 20 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟))
5847, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟)
5952, 52coeq12i 5733 . . . . . . . . . . . . . . . . . . 19 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
6058, 59eqtri 2849 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟𝑟) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∘ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))))
6160, 52sseq12i 4001 . . . . . . . . . . . . . . . . 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 4372 . . . . . . . . . . . . . . . 16 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋}) ↔ 𝑓 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋})))
6647, 65ax-mp 5 . . . . . . . . . . . . . . 15 ([(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]𝑓 = (𝑟 “ {𝑋}) ↔ 𝑓 = (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}))
67 csbima12 5945 . . . . . . . . . . . . . . . . 17 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋})
6852imaeq1i 5924 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟𝑟(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋})
69 csbconstg 3906 . . . . . . . . . . . . . . . . . . 19 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) ∈ V → (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋} = {𝑋})
7047, 69ax-mp 5 . . . . . . . . . . . . . . . . . 18 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋} = {𝑋}
7170imaeq2i 5925 . . . . . . . . . . . . . . . . 17 ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟{𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋})
7267, 68, 713eqtri 2853 . . . . . . . . . . . . . . . 16 (t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟(𝑟 “ {𝑋}) = ((t+‘(𝑅 ∪ ({𝑋} × 𝑓))) “ {𝑋})
7372eqeq2i 2839 . . . . . . . . . . . . . . 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 835 . . . . . . . . . . 11 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → [(t+‘(𝑅 ∪ ({𝑋} × 𝑓))) / 𝑟]((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
7877spesbcd 3870 . . . . . . . . . 10 (((𝑋𝑈𝑌𝑉𝑅𝑊) ∧ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓) → ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
7978ex 413 . . . . . . . . 9 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 → ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋}))))
80 eqeq1 2830 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (𝑔 = (𝑠 “ {𝑋}) ↔ 𝑓 = (𝑠 “ {𝑋})))
8180rexbidv 3302 . . . . . . . . . . 11 (𝑔 = 𝑓 → (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) ↔ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑓 = (𝑠 “ {𝑋})))
82 imaeq1 5922 . . . . . . . . . . . . 13 (𝑠 = 𝑟 → (𝑠 “ {𝑋}) = (𝑟 “ {𝑋}))
8382eqeq2d 2837 . . . . . . . . . . . 12 (𝑠 = 𝑟 → (𝑓 = (𝑠 “ {𝑋}) ↔ 𝑓 = (𝑟 “ {𝑋})))
8483rexab2 3695 . . . . . . . . . . 11 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑓 = (𝑠 “ {𝑋}) ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
8581, 84syl6bb 288 . . . . . . . . . 10 (𝑔 = 𝑓 → (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋}))))
8613, 85elab 3671 . . . . . . . . 9 (𝑓 ∈ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑓 = (𝑟 “ {𝑋})))
8779, 86syl6ibr 253 . . . . . . . 8 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓𝑓 ∈ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})}))
88 intss1 4889 . . . . . . . 8 (𝑓 ∈ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} → {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓)
8987, 88syl6 35 . . . . . . 7 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓))
9089alrimiv 1921 . . . . . 6 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ∀𝑓((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓))
91 ssintab 4891 . . . . . 6 ( {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ↔ ∀𝑓((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ 𝑓))
9290, 91sylibr 235 . . . . 5 ((𝑋𝑈𝑌𝑉𝑅𝑊) → {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ⊆ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
93 ssintab 4891 . . . . . . 7 ( {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} ↔ ∀𝑔(∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ 𝑔))
9482eqeq2d 2837 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝑔 = (𝑠 “ {𝑋}) ↔ 𝑔 = (𝑟 “ {𝑋})))
9594rexab2 3695 . . . . . . . . 9 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) ↔ ∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})))
96 simpr 485 . . . . . . . . . . 11 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → 𝑔 = (𝑟 “ {𝑋}))
97 imass1 5962 . . . . . . . . . . . . . . 15 (𝑅𝑟 → (𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}))
9897adantr 481 . . . . . . . . . . . . . 14 ((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) → (𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}))
99 imass1 5962 . . . . . . . . . . . . . . 15 (𝑅𝑟 → (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ (𝑟 “ {𝑋})))
100 imaco 6102 . . . . . . . . . . . . . . . 16 ((𝑟𝑟) “ {𝑋}) = (𝑟 “ (𝑟 “ {𝑋}))
101 imass1 5962 . . . . . . . . . . . . . . . 16 ((𝑟𝑟) ⊆ 𝑟 → ((𝑟𝑟) “ {𝑋}) ⊆ (𝑟 “ {𝑋}))
102100, 101eqsstrrid 4020 . . . . . . . . . . . . . . 15 ((𝑟𝑟) ⊆ 𝑟 → (𝑟 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))
10399, 102sylan9ss 3984 . . . . . . . . . . . . . 14 ((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) → (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))
10498, 103jca 512 . . . . . . . . . . . . 13 ((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) → ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
105104adantr 481 . . . . . . . . . . . 12 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
106 vex 3503 . . . . . . . . . . . . . 14 𝑟 ∈ V
107106imaex 7609 . . . . . . . . . . . . 13 (𝑟 “ {𝑋}) ∈ V
108 imaundi 6006 . . . . . . . . . . . . . . . 16 (𝑅 “ ({𝑋} ∪ 𝑓)) = ((𝑅 “ {𝑋}) ∪ (𝑅𝑓))
109108sseq1i 3999 . . . . . . . . . . . . . . 15 ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 ↔ ((𝑅 “ {𝑋}) ∪ (𝑅𝑓)) ⊆ 𝑓)
110 unss 4164 . . . . . . . . . . . . . . 15 (((𝑅 “ {𝑋}) ⊆ 𝑓 ∧ (𝑅𝑓) ⊆ 𝑓) ↔ ((𝑅 “ {𝑋}) ∪ (𝑅𝑓)) ⊆ 𝑓)
111109, 110bitr4i 279 . . . . . . . . . . . . . 14 ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 ↔ ((𝑅 “ {𝑋}) ⊆ 𝑓 ∧ (𝑅𝑓) ⊆ 𝑓))
112 imaeq2 5923 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑟 “ {𝑋}) → (𝑅𝑓) = (𝑅 “ (𝑟 “ {𝑋})))
113 id 22 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑟 “ {𝑋}) → 𝑓 = (𝑟 “ {𝑋}))
114112, 113sseq12d 4004 . . . . . . . . . . . . . . 15 (𝑓 = (𝑟 “ {𝑋}) → ((𝑅𝑓) ⊆ 𝑓 ↔ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
115114cleq2lem 39836 . . . . . . . . . . . . . 14 (𝑓 = (𝑟 “ {𝑋}) → (((𝑅 “ {𝑋}) ⊆ 𝑓 ∧ (𝑅𝑓) ⊆ 𝑓) ↔ ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))))
116111, 115syl5bb 284 . . . . . . . . . . . . 13 (𝑓 = (𝑟 “ {𝑋}) → ((𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓 ↔ ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋}))))
117107, 116elab 3671 . . . . . . . . . . . 12 ((𝑟 “ {𝑋}) ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ↔ ((𝑅 “ {𝑋}) ⊆ (𝑟 “ {𝑋}) ∧ (𝑅 “ (𝑟 “ {𝑋})) ⊆ (𝑟 “ {𝑋})))
118105, 117sylibr 235 . . . . . . . . . . 11 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → (𝑟 “ {𝑋}) ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
11996, 118eqeltrd 2918 . . . . . . . . . 10 (((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → 𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
120119exlimiv 1924 . . . . . . . . 9 (∃𝑟((𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ∧ 𝑔 = (𝑟 “ {𝑋})) → 𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
12195, 120sylbi 218 . . . . . . . 8 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) → 𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
122 intss1 4889 . . . . . . . 8 (𝑔 ∈ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ 𝑔)
123121, 122syl 17 . . . . . . 7 (∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋}) → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ 𝑔)
12493, 123mpgbir 1793 . . . . . 6 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})}
125124a1i 11 . . . . 5 ((𝑋𝑈𝑌𝑉𝑅𝑊) → {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓} ⊆ {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})})
12692, 125eqssd 3988 . . . 4 ((𝑋𝑈𝑌𝑉𝑅𝑊) → {𝑔 ∣ ∃𝑠 ∈ {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}𝑔 = (𝑠 “ {𝑋})} = {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
12710, 126eqtrd 2861 . . 3 ((𝑋𝑈𝑌𝑉𝑅𝑊) → ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) = {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})
128127eleq2d 2903 . 2 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑌 ∈ ( {𝑟 ∣ (𝑅𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} “ {𝑋}) ↔ 𝑌 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
1298, 128bitrd 280 1 ((𝑋𝑈𝑌𝑉𝑅𝑊) → (𝑋(t+‘𝑅)𝑌𝑌 {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081  wal 1528   = wceq 1530  wex 1773  wcel 2107  {cab 2804  wne 3021  wrex 3144  Vcvv 3500  [wsbc 3776  csb 3887  cun 3938  cin 3939  wss 3940  c0 4295  {csn 4564  cop 4570   cint 4874   class class class wbr 5063   × cxp 5552  ran crn 5555  cima 5557  ccom 5558  cfv 6352  t+ctcl 14335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-n0 11887  df-z 11971  df-uz 12233  df-seq 13360  df-trcl 14337  df-relexp 14370
This theorem is referenced by:  dffrege76  40153
  Copyright terms: Public domain W3C validator