Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ofpreima2 Structured version   Visualization version   GIF version

Theorem ofpreima2 31891
Description: Express the preimage of a function operation as a union of preimages. This version of ofpreima 31890 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.)
Hypotheses
Ref Expression
ofpreima.1 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
ofpreima.2 (πœ‘ β†’ 𝐺:𝐴⟢𝐢)
ofpreima.3 (πœ‘ β†’ 𝐴 ∈ 𝑉)
ofpreima.4 (πœ‘ β†’ 𝑅 Fn (𝐡 Γ— 𝐢))
Assertion
Ref Expression
ofpreima2 (πœ‘ β†’ (β—‘(𝐹 ∘f 𝑅𝐺) β€œ 𝐷) = βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
Distinct variable groups:   𝐴,𝑝   𝐷,𝑝   𝐹,𝑝   𝐺,𝑝   𝑅,𝑝   πœ‘,𝑝
Allowed substitution hints:   𝐡(𝑝)   𝐢(𝑝)   𝑉(𝑝)

Proof of Theorem ofpreima2
StepHypRef Expression
1 ofpreima.1 . . . 4 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
2 ofpreima.2 . . . 4 (πœ‘ β†’ 𝐺:𝐴⟢𝐢)
3 ofpreima.3 . . . 4 (πœ‘ β†’ 𝐴 ∈ 𝑉)
4 ofpreima.4 . . . 4 (πœ‘ β†’ 𝑅 Fn (𝐡 Γ— 𝐢))
51, 2, 3, 4ofpreima 31890 . . 3 (πœ‘ β†’ (β—‘(𝐹 ∘f 𝑅𝐺) β€œ 𝐷) = βˆͺ 𝑝 ∈ (◑𝑅 β€œ 𝐷)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
6 inundif 4479 . . . . 5 (((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺)) βˆͺ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) = (◑𝑅 β€œ 𝐷)
7 iuneq1 5014 . . . . 5 ((((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺)) βˆͺ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) = (◑𝑅 β€œ 𝐷) β†’ βˆͺ 𝑝 ∈ (((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺)) βˆͺ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺)))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆͺ 𝑝 ∈ (◑𝑅 β€œ 𝐷)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
86, 7ax-mp 5 . . . 4 βˆͺ 𝑝 ∈ (((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺)) βˆͺ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺)))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆͺ 𝑝 ∈ (◑𝑅 β€œ 𝐷)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))
9 iunxun 5098 . . . 4 βˆͺ 𝑝 ∈ (((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺)) βˆͺ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺)))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
108, 9eqtr3i 2763 . . 3 βˆͺ 𝑝 ∈ (◑𝑅 β€œ 𝐷)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
115, 10eqtrdi 2789 . 2 (πœ‘ β†’ (β—‘(𝐹 ∘f 𝑅𝐺) β€œ 𝐷) = (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
12 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺)))
1312eldifbd 3962 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ Β¬ 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺))
14 cnvimass 6081 . . . . . . . . . . . . . 14 (◑𝑅 β€œ 𝐷) βŠ† dom 𝑅
154fndmd 6655 . . . . . . . . . . . . . 14 (πœ‘ β†’ dom 𝑅 = (𝐡 Γ— 𝐢))
1614, 15sseqtrid 4035 . . . . . . . . . . . . 13 (πœ‘ β†’ (◑𝑅 β€œ 𝐷) βŠ† (𝐡 Γ— 𝐢))
1716ssdifssd 4143 . . . . . . . . . . . 12 (πœ‘ β†’ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺)) βŠ† (𝐡 Γ— 𝐢))
1817sselda 3983 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (𝐡 Γ— 𝐢))
19 1st2nd2 8014 . . . . . . . . . . 11 (𝑝 ∈ (𝐡 Γ— 𝐢) β†’ 𝑝 = ⟨(1st β€˜π‘), (2nd β€˜π‘)⟩)
20 elxp6 8009 . . . . . . . . . . . 12 (𝑝 ∈ (ran 𝐹 Γ— ran 𝐺) ↔ (𝑝 = ⟨(1st β€˜π‘), (2nd β€˜π‘)⟩ ∧ ((1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺)))
2120simplbi2 502 . . . . . . . . . . 11 (𝑝 = ⟨(1st β€˜π‘), (2nd β€˜π‘)⟩ β†’ (((1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺) β†’ 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺)))
2218, 19, 213syl 18 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ (((1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺) β†’ 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺)))
2313, 22mtod 197 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ Β¬ ((1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺))
24 ianor 981 . . . . . . . . 9 (Β¬ ((1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺) ↔ (Β¬ (1st β€˜π‘) ∈ ran 𝐹 ∨ Β¬ (2nd β€˜π‘) ∈ ran 𝐺))
2523, 24sylib 217 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ (Β¬ (1st β€˜π‘) ∈ ran 𝐹 ∨ Β¬ (2nd β€˜π‘) ∈ ran 𝐺))
26 disjsn 4716 . . . . . . . . 9 ((ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ… ↔ Β¬ (1st β€˜π‘) ∈ ran 𝐹)
27 disjsn 4716 . . . . . . . . 9 ((ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ… ↔ Β¬ (2nd β€˜π‘) ∈ ran 𝐺)
2826, 27orbi12i 914 . . . . . . . 8 (((ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ… ∨ (ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ…) ↔ (Β¬ (1st β€˜π‘) ∈ ran 𝐹 ∨ Β¬ (2nd β€˜π‘) ∈ ran 𝐺))
2925, 28sylibr 233 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ ((ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ… ∨ (ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ…))
301ffnd 6719 . . . . . . . . 9 (πœ‘ β†’ 𝐹 Fn 𝐴)
31 dffn3 6731 . . . . . . . . 9 (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟢ran 𝐹)
3230, 31sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝐹:𝐴⟢ran 𝐹)
332ffnd 6719 . . . . . . . . . 10 (πœ‘ β†’ 𝐺 Fn 𝐴)
34 dffn3 6731 . . . . . . . . . 10 (𝐺 Fn 𝐴 ↔ 𝐺:𝐴⟢ran 𝐺)
3533, 34sylib 217 . . . . . . . . 9 (πœ‘ β†’ 𝐺:𝐴⟢ran 𝐺)
3635adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ 𝐺:𝐴⟢ran 𝐺)
37 fimacnvdisj 6770 . . . . . . . . . . 11 ((𝐹:𝐴⟢ran 𝐹 ∧ (ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ…) β†’ (◑𝐹 β€œ {(1st β€˜π‘)}) = βˆ…)
38 ineq1 4206 . . . . . . . . . . . 12 ((◑𝐹 β€œ {(1st β€˜π‘)}) = βˆ… β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = (βˆ… ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
39 0in 4394 . . . . . . . . . . . 12 (βˆ… ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…
4038, 39eqtrdi 2789 . . . . . . . . . . 11 ((◑𝐹 β€œ {(1st β€˜π‘)}) = βˆ… β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…)
4137, 40syl 17 . . . . . . . . . 10 ((𝐹:𝐴⟢ran 𝐹 ∧ (ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ…) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…)
4241ex 414 . . . . . . . . 9 (𝐹:𝐴⟢ran 𝐹 β†’ ((ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ… β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…))
43 fimacnvdisj 6770 . . . . . . . . . . 11 ((𝐺:𝐴⟢ran 𝐺 ∧ (ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ…) β†’ (◑𝐺 β€œ {(2nd β€˜π‘)}) = βˆ…)
44 ineq2 4207 . . . . . . . . . . . 12 ((◑𝐺 β€œ {(2nd β€˜π‘)}) = βˆ… β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ βˆ…))
45 in0 4392 . . . . . . . . . . . 12 ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ βˆ…) = βˆ…
4644, 45eqtrdi 2789 . . . . . . . . . . 11 ((◑𝐺 β€œ {(2nd β€˜π‘)}) = βˆ… β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…)
4743, 46syl 17 . . . . . . . . . 10 ((𝐺:𝐴⟢ran 𝐺 ∧ (ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ…) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…)
4847ex 414 . . . . . . . . 9 (𝐺:𝐴⟢ran 𝐺 β†’ ((ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ… β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…))
4942, 48jaao 954 . . . . . . . 8 ((𝐹:𝐴⟢ran 𝐹 ∧ 𝐺:𝐴⟢ran 𝐺) β†’ (((ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ… ∨ (ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ…) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…))
5032, 36, 49syl2an2r 684 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ (((ran 𝐹 ∩ {(1st β€˜π‘)}) = βˆ… ∨ (ran 𝐺 ∩ {(2nd β€˜π‘)}) = βˆ…) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…))
5129, 50mpd 15 . . . . . 6 ((πœ‘ ∧ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…)
5251iuneq2dv 5022 . . . . 5 (πœ‘ β†’ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))βˆ…)
53 iun0 5066 . . . . 5 βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))βˆ… = βˆ…
5452, 53eqtrdi 2789 . . . 4 (πœ‘ β†’ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) = βˆ…)
5554uneq2d 4164 . . 3 (πœ‘ β†’ (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆ…))
56 un0 4391 . . 3 (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆ…) = βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))
5755, 56eqtrdi 2789 . 2 (πœ‘ β†’ (βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) βˆͺ βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) βˆ– (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
5811, 57eqtrd 2773 1 (πœ‘ β†’ (β—‘(𝐹 ∘f 𝑅𝐺) β€œ 𝐷) = βˆͺ 𝑝 ∈ ((◑𝑅 β€œ 𝐷) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948  βˆ…c0 4323  {csn 4629  βŸ¨cop 4635  βˆͺ ciun 4998   Γ— cxp 5675  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β€œ cima 5680   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∘f cof 7668  1st c1st 7973  2nd c2nd 7974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-1st 7975  df-2nd 7976
This theorem is referenced by:  sibfof  33339
  Copyright terms: Public domain W3C validator