ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  setscom GIF version

Theorem setscom 12009
Description: Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
Hypotheses
Ref Expression
setscom.1 𝐴 ∈ V
setscom.2 𝐵 ∈ V
Assertion
Ref Expression
setscom (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))

Proof of Theorem setscom
StepHypRef Expression
1 rescom 4844 . . . . . 6 ((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) = ((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴}))
21uneq1i 3226 . . . . 5 (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩})
32uneq1i 3226 . . . 4 ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩})
4 un23 3235 . . . 4 ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}) ∪ {⟨𝐴, 𝐶⟩})
53, 4eqtri 2160 . . 3 ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}) ∪ {⟨𝐴, 𝐶⟩})
6 setscom.1 . . . . . . . 8 𝐴 ∈ V
7 setsvala 12000 . . . . . . . 8 ((𝑆𝑉𝐴 ∈ V ∧ 𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
86, 7mp3an2 1303 . . . . . . 7 ((𝑆𝑉𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
98ad2ant2r 500 . . . . . 6 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (𝑆 sSet ⟨𝐴, 𝐶⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
109reseq1d 4818 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ↾ (V ∖ {𝐵})))
11 resundir 4833 . . . . . 6 (((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵})))
12 elex 2697 . . . . . . . . . . 11 (𝐶𝑊𝐶 ∈ V)
1312ad2antrl 481 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐶 ∈ V)
14 opelxpi 4571 . . . . . . . . . 10 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → ⟨𝐴, 𝐶⟩ ∈ (V × V))
156, 13, 14sylancr 410 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐴, 𝐶⟩ ∈ (V × V))
16 opexg 4150 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → ⟨𝐴, 𝐶⟩ ∈ V)
176, 13, 16sylancr 410 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐴, 𝐶⟩ ∈ V)
18 relsng 4642 . . . . . . . . . 10 (⟨𝐴, 𝐶⟩ ∈ V → (Rel {⟨𝐴, 𝐶⟩} ↔ ⟨𝐴, 𝐶⟩ ∈ (V × V)))
1917, 18syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (Rel {⟨𝐴, 𝐶⟩} ↔ ⟨𝐴, 𝐶⟩ ∈ (V × V)))
2015, 19mpbird 166 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → Rel {⟨𝐴, 𝐶⟩})
21 dmsnopg 5010 . . . . . . . . . 10 (𝐶 ∈ V → dom {⟨𝐴, 𝐶⟩} = {𝐴})
2213, 21syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐴, 𝐶⟩} = {𝐴})
23 disjsn2 3586 . . . . . . . . . . 11 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
2423ad2antlr 480 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ({𝐴} ∩ {𝐵}) = ∅)
25 disj2 3418 . . . . . . . . . 10 (({𝐴} ∩ {𝐵}) = ∅ ↔ {𝐴} ⊆ (V ∖ {𝐵}))
2624, 25sylib 121 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → {𝐴} ⊆ (V ∖ {𝐵}))
2722, 26eqsstrd 3133 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐴, 𝐶⟩} ⊆ (V ∖ {𝐵}))
28 relssres 4857 . . . . . . . 8 ((Rel {⟨𝐴, 𝐶⟩} ∧ dom {⟨𝐴, 𝐶⟩} ⊆ (V ∖ {𝐵})) → ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵})) = {⟨𝐴, 𝐶⟩})
2920, 27, 28syl2anc 408 . . . . . . 7 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵})) = {⟨𝐴, 𝐶⟩})
3029uneq2d 3230 . . . . . 6 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵}))) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}))
3111, 30syl5eq 2184 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}))
3210, 31eqtrd 2172 . . . 4 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}))
3332uneq1d 3229 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}))
34 setscom.2 . . . . . . . 8 𝐵 ∈ V
35 setsvala 12000 . . . . . . . 8 ((𝑆𝑉𝐵 ∈ V ∧ 𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) = ((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
3634, 35mp3an2 1303 . . . . . . 7 ((𝑆𝑉𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) = ((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
3736reseq1d 4818 . . . . . 6 ((𝑆𝑉𝐷𝑋) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})))
3837ad2ant2rl 502 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})))
39 resundir 4833 . . . . . 6 (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴})))
40 elex 2697 . . . . . . . . . . 11 (𝐷𝑋𝐷 ∈ V)
4140ad2antll 482 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐷 ∈ V)
42 opelxpi 4571 . . . . . . . . . 10 ((𝐵 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐵, 𝐷⟩ ∈ (V × V))
4334, 41, 42sylancr 410 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐵, 𝐷⟩ ∈ (V × V))
44 opexg 4150 . . . . . . . . . . 11 ((𝐵 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐵, 𝐷⟩ ∈ V)
4534, 41, 44sylancr 410 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐵, 𝐷⟩ ∈ V)
46 relsng 4642 . . . . . . . . . 10 (⟨𝐵, 𝐷⟩ ∈ V → (Rel {⟨𝐵, 𝐷⟩} ↔ ⟨𝐵, 𝐷⟩ ∈ (V × V)))
4745, 46syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (Rel {⟨𝐵, 𝐷⟩} ↔ ⟨𝐵, 𝐷⟩ ∈ (V × V)))
4843, 47mpbird 166 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → Rel {⟨𝐵, 𝐷⟩})
49 dmsnopg 5010 . . . . . . . . . 10 (𝐷 ∈ V → dom {⟨𝐵, 𝐷⟩} = {𝐵})
5041, 49syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐵, 𝐷⟩} = {𝐵})
51 ssv 3119 . . . . . . . . . . 11 {𝐴} ⊆ V
52 ssv 3119 . . . . . . . . . . 11 {𝐵} ⊆ V
53 ssconb 3209 . . . . . . . . . . 11 (({𝐴} ⊆ V ∧ {𝐵} ⊆ V) → ({𝐴} ⊆ (V ∖ {𝐵}) ↔ {𝐵} ⊆ (V ∖ {𝐴})))
5451, 52, 53mp2an 422 . . . . . . . . . 10 ({𝐴} ⊆ (V ∖ {𝐵}) ↔ {𝐵} ⊆ (V ∖ {𝐴}))
5526, 54sylib 121 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → {𝐵} ⊆ (V ∖ {𝐴}))
5650, 55eqsstrd 3133 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐵, 𝐷⟩} ⊆ (V ∖ {𝐴}))
57 relssres 4857 . . . . . . . 8 ((Rel {⟨𝐵, 𝐷⟩} ∧ dom {⟨𝐵, 𝐷⟩} ⊆ (V ∖ {𝐴})) → ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐷⟩})
5848, 56, 57syl2anc 408 . . . . . . 7 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐷⟩})
5958uneq2d 3230 . . . . . 6 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴}))) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}))
6039, 59syl5eq 2184 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}))
6138, 60eqtrd 2172 . . . 4 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}))
6261uneq1d 3229 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}) ∪ {⟨𝐴, 𝐶⟩}))
635, 33, 623eqtr4a 2198 . 2 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) = (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
64 setsex 12001 . . . . 5 ((𝑆𝑉𝐴 ∈ V ∧ 𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V)
656, 64mp3an2 1303 . . . 4 ((𝑆𝑉𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V)
6665ad2ant2r 500 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V)
6734a1i 9 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐵 ∈ V)
68 simprr 521 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐷𝑋)
69 setsvala 12000 . . 3 (((𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V ∧ 𝐵 ∈ V ∧ 𝐷𝑋) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
7066, 67, 68, 69syl3anc 1216 . 2 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
71 setsex 12001 . . . . 5 ((𝑆𝑉𝐵 ∈ V ∧ 𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V)
7234, 71mp3an2 1303 . . . 4 ((𝑆𝑉𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V)
7372ad2ant2rl 502 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V)
746a1i 9 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐴 ∈ V)
75 simprl 520 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐶𝑊)
76 setsvala 12000 . . 3 (((𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V ∧ 𝐴 ∈ V ∧ 𝐶𝑊) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩) = (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
7773, 74, 75, 76syl3anc 1216 . 2 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩) = (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
7863, 70, 773eqtr4d 2182 1 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1331  wcel 1480  wne 2308  Vcvv 2686  cdif 3068  cun 3069  cin 3070  wss 3071  c0 3363  {csn 3527  cop 3530   × cxp 4537  dom cdm 4539  cres 4541  Rel wrel 4544  (class class class)co 5774   sSet csts 11967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-res 4551  df-iota 5088  df-fun 5125  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-sets 11976
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator