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

Theorem setscom 12520
Description: Different components can be set in any order. (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 4947 . . . . . 6 ((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) = ((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴}))
21uneq1i 3300 . . . . 5 (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩})
32uneq1i 3300 . . . 4 ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩})
4 un23 3309 . . . 4 ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}) ∪ {⟨𝐴, 𝐶⟩})
53, 4eqtri 2210 . . 3 ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}) ∪ {⟨𝐴, 𝐶⟩})
6 setscom.1 . . . . . . . 8 𝐴 ∈ V
7 setsvala 12511 . . . . . . . 8 ((𝑆𝑉𝐴 ∈ V ∧ 𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
86, 7mp3an2 1336 . . . . . . 7 ((𝑆𝑉𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
98ad2ant2r 509 . . . . . 6 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (𝑆 sSet ⟨𝐴, 𝐶⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
109reseq1d 4921 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ↾ (V ∖ {𝐵})))
11 resundir 4936 . . . . . 6 (((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵})))
12 elex 2763 . . . . . . . . . . 11 (𝐶𝑊𝐶 ∈ V)
1312ad2antrl 490 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐶 ∈ V)
14 opelxpi 4673 . . . . . . . . . 10 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → ⟨𝐴, 𝐶⟩ ∈ (V × V))
156, 13, 14sylancr 414 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐴, 𝐶⟩ ∈ (V × V))
16 opexg 4243 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → ⟨𝐴, 𝐶⟩ ∈ V)
176, 13, 16sylancr 414 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐴, 𝐶⟩ ∈ V)
18 relsng 4744 . . . . . . . . . 10 (⟨𝐴, 𝐶⟩ ∈ V → (Rel {⟨𝐴, 𝐶⟩} ↔ ⟨𝐴, 𝐶⟩ ∈ (V × V)))
1917, 18syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (Rel {⟨𝐴, 𝐶⟩} ↔ ⟨𝐴, 𝐶⟩ ∈ (V × V)))
2015, 19mpbird 167 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → Rel {⟨𝐴, 𝐶⟩})
21 dmsnopg 5115 . . . . . . . . . 10 (𝐶 ∈ V → dom {⟨𝐴, 𝐶⟩} = {𝐴})
2213, 21syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐴, 𝐶⟩} = {𝐴})
23 disjsn2 3670 . . . . . . . . . . 11 (𝐴𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
2423ad2antlr 489 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ({𝐴} ∩ {𝐵}) = ∅)
25 disj2 3493 . . . . . . . . . 10 (({𝐴} ∩ {𝐵}) = ∅ ↔ {𝐴} ⊆ (V ∖ {𝐵}))
2624, 25sylib 122 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → {𝐴} ⊆ (V ∖ {𝐵}))
2722, 26eqsstrd 3206 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐴, 𝐶⟩} ⊆ (V ∖ {𝐵}))
28 relssres 4960 . . . . . . . 8 ((Rel {⟨𝐴, 𝐶⟩} ∧ dom {⟨𝐴, 𝐶⟩} ⊆ (V ∖ {𝐵})) → ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵})) = {⟨𝐴, 𝐶⟩})
2920, 27, 28syl2anc 411 . . . . . . 7 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵})) = {⟨𝐴, 𝐶⟩})
3029uneq2d 3304 . . . . . 6 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ ({⟨𝐴, 𝐶⟩} ↾ (V ∖ {𝐵}))) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}))
3111, 30eqtrid 2234 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}))
3210, 31eqtrd 2222 . . . 4 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}))
3332uneq1d 3303 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) = ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {⟨𝐴, 𝐶⟩}) ∪ {⟨𝐵, 𝐷⟩}))
34 setscom.2 . . . . . . . 8 𝐵 ∈ V
35 setsvala 12511 . . . . . . . 8 ((𝑆𝑉𝐵 ∈ V ∧ 𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) = ((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
3634, 35mp3an2 1336 . . . . . . 7 ((𝑆𝑉𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) = ((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
3736reseq1d 4921 . . . . . 6 ((𝑆𝑉𝐷𝑋) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})))
3837ad2ant2rl 511 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})))
39 resundir 4936 . . . . . 6 (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴})))
40 elex 2763 . . . . . . . . . . 11 (𝐷𝑋𝐷 ∈ V)
4140ad2antll 491 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐷 ∈ V)
42 opelxpi 4673 . . . . . . . . . 10 ((𝐵 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐵, 𝐷⟩ ∈ (V × V))
4334, 41, 42sylancr 414 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐵, 𝐷⟩ ∈ (V × V))
44 opexg 4243 . . . . . . . . . . 11 ((𝐵 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐵, 𝐷⟩ ∈ V)
4534, 41, 44sylancr 414 . . . . . . . . . 10 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ⟨𝐵, 𝐷⟩ ∈ V)
46 relsng 4744 . . . . . . . . . 10 (⟨𝐵, 𝐷⟩ ∈ V → (Rel {⟨𝐵, 𝐷⟩} ↔ ⟨𝐵, 𝐷⟩ ∈ (V × V)))
4745, 46syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (Rel {⟨𝐵, 𝐷⟩} ↔ ⟨𝐵, 𝐷⟩ ∈ (V × V)))
4843, 47mpbird 167 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → Rel {⟨𝐵, 𝐷⟩})
49 dmsnopg 5115 . . . . . . . . . 10 (𝐷 ∈ V → dom {⟨𝐵, 𝐷⟩} = {𝐵})
5041, 49syl 14 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐵, 𝐷⟩} = {𝐵})
51 ssv 3192 . . . . . . . . . . 11 {𝐴} ⊆ V
52 ssv 3192 . . . . . . . . . . 11 {𝐵} ⊆ V
53 ssconb 3283 . . . . . . . . . . 11 (({𝐴} ⊆ V ∧ {𝐵} ⊆ V) → ({𝐴} ⊆ (V ∖ {𝐵}) ↔ {𝐵} ⊆ (V ∖ {𝐴})))
5451, 52, 53mp2an 426 . . . . . . . . . 10 ({𝐴} ⊆ (V ∖ {𝐵}) ↔ {𝐵} ⊆ (V ∖ {𝐴}))
5526, 54sylib 122 . . . . . . . . 9 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → {𝐵} ⊆ (V ∖ {𝐴}))
5650, 55eqsstrd 3206 . . . . . . . 8 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → dom {⟨𝐵, 𝐷⟩} ⊆ (V ∖ {𝐴}))
57 relssres 4960 . . . . . . . 8 ((Rel {⟨𝐵, 𝐷⟩} ∧ dom {⟨𝐵, 𝐷⟩} ⊆ (V ∖ {𝐴})) → ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐷⟩})
5848, 56, 57syl2anc 411 . . . . . . 7 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐷⟩})
5958uneq2d 3304 . . . . . 6 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐵, 𝐷⟩} ↾ (V ∖ {𝐴}))) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}))
6039, 59eqtrid 2234 . . . . 5 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}))
6138, 60eqtrd 2222 . . . 4 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}))
6261uneq1d 3303 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {⟨𝐵, 𝐷⟩}) ∪ {⟨𝐴, 𝐶⟩}))
635, 33, 623eqtr4a 2248 . 2 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}) = (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
64 setsex 12512 . . . . 5 ((𝑆𝑉𝐴 ∈ V ∧ 𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V)
656, 64mp3an2 1336 . . . 4 ((𝑆𝑉𝐶𝑊) → (𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V)
6665ad2ant2r 509 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V)
6734a1i 9 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐵 ∈ V)
68 simprr 531 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐷𝑋)
69 setsvala 12511 . . 3 (((𝑆 sSet ⟨𝐴, 𝐶⟩) ∈ V ∧ 𝐵 ∈ V ∧ 𝐷𝑋) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
7066, 67, 68, 69syl3anc 1249 . 2 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = (((𝑆 sSet ⟨𝐴, 𝐶⟩) ↾ (V ∖ {𝐵})) ∪ {⟨𝐵, 𝐷⟩}))
71 setsex 12512 . . . . 5 ((𝑆𝑉𝐵 ∈ V ∧ 𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V)
7234, 71mp3an2 1336 . . . 4 ((𝑆𝑉𝐷𝑋) → (𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V)
7372ad2ant2rl 511 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → (𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V)
746a1i 9 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐴 ∈ V)
75 simprl 529 . . 3 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → 𝐶𝑊)
76 setsvala 12511 . . 3 (((𝑆 sSet ⟨𝐵, 𝐷⟩) ∈ V ∧ 𝐴 ∈ V ∧ 𝐶𝑊) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩) = (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
7773, 74, 75, 76syl3anc 1249 . 2 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩) = (((𝑆 sSet ⟨𝐵, 𝐷⟩) ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐶⟩}))
7863, 70, 773eqtr4d 2232 1 (((𝑆𝑉𝐴𝐵) ∧ (𝐶𝑊𝐷𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1364  wcel 2160  wne 2360  Vcvv 2752  cdif 3141  cun 3142  cin 3143  wss 3144  c0 3437  {csn 3607  cop 3610   × cxp 4639  dom cdm 4641  cres 4643  Rel wrel 4646  (class class class)co 5891   sSet csts 12478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-res 4653  df-iota 5193  df-fun 5233  df-fv 5239  df-ov 5894  df-oprab 5895  df-mpo 5896  df-sets 12487
This theorem is referenced by:  setscomd  12521
  Copyright terms: Public domain W3C validator