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

Theorem fpwrelmapffslem 32743
Description: Lemma for fpwrelmapffs 32745. For this theorem, the sets 𝐴 and 𝐵 could be infinite, but the relation 𝑅 itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
Hypotheses
Ref Expression
fpwrelmapffslem.1 𝐴 ∈ V
fpwrelmapffslem.2 𝐵 ∈ V
fpwrelmapffslem.3 (𝜑𝐹:𝐴⟶𝒫 𝐵)
fpwrelmapffslem.4 (𝜑𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))})
Assertion
Ref Expression
fpwrelmapffslem (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem fpwrelmapffslem
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwrelmapffslem.4 . . 3 (𝜑𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))})
2 relopabv 5831 . . . 4 Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}
3 releq 5786 . . . 4 (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} → (Rel 𝑅 ↔ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))}))
42, 3mpbiri 258 . . 3 (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} → Rel 𝑅)
5 relfi 32615 . . 3 (Rel 𝑅 → (𝑅 ∈ Fin ↔ (dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin)))
61, 4, 53syl 18 . 2 (𝜑 → (𝑅 ∈ Fin ↔ (dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin)))
7 rexcom4 3288 . . . . . . . . . . . . 13 (∃𝑥𝐴𝑧(𝑤𝑧𝑧 = (𝐹𝑥)) ↔ ∃𝑧𝑥𝐴 (𝑤𝑧𝑧 = (𝐹𝑥)))
8 ancom 460 . . . . . . . . . . . . . . . 16 ((𝑧 = (𝐹𝑥) ∧ 𝑤𝑧) ↔ (𝑤𝑧𝑧 = (𝐹𝑥)))
98exbii 1848 . . . . . . . . . . . . . . 15 (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑤𝑧) ↔ ∃𝑧(𝑤𝑧𝑧 = (𝐹𝑥)))
10 fvex 6919 . . . . . . . . . . . . . . . 16 (𝐹𝑥) ∈ V
11 eleq2 2830 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐹𝑥) → (𝑤𝑧𝑤 ∈ (𝐹𝑥)))
1210, 11ceqsexv 3532 . . . . . . . . . . . . . . 15 (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑤𝑧) ↔ 𝑤 ∈ (𝐹𝑥))
139, 12bitr3i 277 . . . . . . . . . . . . . 14 (∃𝑧(𝑤𝑧𝑧 = (𝐹𝑥)) ↔ 𝑤 ∈ (𝐹𝑥))
1413rexbii 3094 . . . . . . . . . . . . 13 (∃𝑥𝐴𝑧(𝑤𝑧𝑧 = (𝐹𝑥)) ↔ ∃𝑥𝐴 𝑤 ∈ (𝐹𝑥))
15 r19.42v 3191 . . . . . . . . . . . . . 14 (∃𝑥𝐴 (𝑤𝑧𝑧 = (𝐹𝑥)) ↔ (𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = (𝐹𝑥)))
1615exbii 1848 . . . . . . . . . . . . 13 (∃𝑧𝑥𝐴 (𝑤𝑧𝑧 = (𝐹𝑥)) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = (𝐹𝑥)))
177, 14, 163bitr3ri 302 . . . . . . . . . . . 12 (∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = (𝐹𝑥)) ↔ ∃𝑥𝐴 𝑤 ∈ (𝐹𝑥))
18 df-rex 3071 . . . . . . . . . . . 12 (∃𝑥𝐴 𝑤 ∈ (𝐹𝑥) ↔ ∃𝑥(𝑥𝐴𝑤 ∈ (𝐹𝑥)))
1917, 18bitr2i 276 . . . . . . . . . . 11 (∃𝑥(𝑥𝐴𝑤 ∈ (𝐹𝑥)) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = (𝐹𝑥)))
2019a1i 11 . . . . . . . . . 10 (𝜑 → (∃𝑥(𝑥𝐴𝑤 ∈ (𝐹𝑥)) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = (𝐹𝑥))))
21 vex 3484 . . . . . . . . . . 11 𝑤 ∈ V
22 eleq1w 2824 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (𝑦 ∈ (𝐹𝑥) ↔ 𝑤 ∈ (𝐹𝑥)))
2322anbi2d 630 . . . . . . . . . . . 12 (𝑦 = 𝑤 → ((𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴𝑤 ∈ (𝐹𝑥))))
2423exbidv 1921 . . . . . . . . . . 11 (𝑦 = 𝑤 → (∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ ∃𝑥(𝑥𝐴𝑤 ∈ (𝐹𝑥))))
2521, 24elab 3679 . . . . . . . . . 10 (𝑤 ∈ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ↔ ∃𝑥(𝑥𝐴𝑤 ∈ (𝐹𝑥)))
26 eluniab 4921 . . . . . . . . . 10 (𝑤 {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = (𝐹𝑥)))
2720, 25, 263bitr4g 314 . . . . . . . . 9 (𝜑 → (𝑤 ∈ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ↔ 𝑤 {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)}))
2827eqrdv 2735 . . . . . . . 8 (𝜑 → {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)})
2928eleq1d 2826 . . . . . . 7 (𝜑 → ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ∈ Fin ↔ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin))
3029adantr 480 . . . . . 6 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ∈ Fin ↔ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin))
31 fpwrelmapffslem.3 . . . . . . . . . . 11 (𝜑𝐹:𝐴⟶𝒫 𝐵)
32 ffn 6736 . . . . . . . . . . 11 (𝐹:𝐴⟶𝒫 𝐵𝐹 Fn 𝐴)
33 fnrnfv 6968 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)})
3431, 32, 333syl 18 . . . . . . . . . 10 (𝜑 → ran 𝐹 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)})
3534adantr 480 . . . . . . . . 9 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ran 𝐹 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)})
36 0ex 5307 . . . . . . . . . . 11 ∅ ∈ V
3736a1i 11 . . . . . . . . . 10 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ∅ ∈ V)
38 fpwrelmapffslem.1 . . . . . . . . . . . 12 𝐴 ∈ V
39 fex 7246 . . . . . . . . . . . 12 ((𝐹:𝐴⟶𝒫 𝐵𝐴 ∈ V) → 𝐹 ∈ V)
4031, 38, 39sylancl 586 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
4140adantr 480 . . . . . . . . . 10 ((𝜑 ∧ dom 𝑅 ∈ Fin) → 𝐹 ∈ V)
4231ffund 6740 . . . . . . . . . . 11 (𝜑 → Fun 𝐹)
4342adantr 480 . . . . . . . . . 10 ((𝜑 ∧ dom 𝑅 ∈ Fin) → Fun 𝐹)
44 opabdm 32623 . . . . . . . . . . . . . 14 (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} → dom 𝑅 = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))})
451, 44syl 17 . . . . . . . . . . . . 13 (𝜑 → dom 𝑅 = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))})
4638, 39mpan2 691 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴⟶𝒫 𝐵𝐹 ∈ V)
47 suppimacnv 8199 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ V ∧ ∅ ∈ V) → (𝐹 supp ∅) = (𝐹 “ (V ∖ {∅})))
4836, 47mpan2 691 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ V → (𝐹 supp ∅) = (𝐹 “ (V ∖ {∅})))
4931, 46, 483syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 supp ∅) = (𝐹 “ (V ∖ {∅})))
5031feqmptd 6977 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
5150cnveqd 5886 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
5251imaeq1d 6077 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 “ (V ∖ {∅})) = ((𝑥𝐴 ↦ (𝐹𝑥)) “ (V ∖ {∅})))
5349, 52eqtrd 2777 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) = ((𝑥𝐴 ↦ (𝐹𝑥)) “ (V ∖ {∅})))
54 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐹𝑥))
5554mptpreima 6258 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ↦ (𝐹𝑥)) “ (V ∖ {∅})) = {𝑥𝐴 ∣ (𝐹𝑥) ∈ (V ∖ {∅})}
5653, 55eqtrdi 2793 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 supp ∅) = {𝑥𝐴 ∣ (𝐹𝑥) ∈ (V ∖ {∅})})
57 suppvalfn 8193 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝐴𝐴 ∈ V ∧ ∅ ∈ V) → (𝐹 supp ∅) = {𝑥𝐴 ∣ (𝐹𝑥) ≠ ∅})
5838, 36, 57mp3an23 1455 . . . . . . . . . . . . . . . 16 (𝐹 Fn 𝐴 → (𝐹 supp ∅) = {𝑥𝐴 ∣ (𝐹𝑥) ≠ ∅})
5931, 32, 583syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) = {𝑥𝐴 ∣ (𝐹𝑥) ≠ ∅})
60 n0 4353 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹𝑥))
6160rabbii 3442 . . . . . . . . . . . . . . . 16 {𝑥𝐴 ∣ (𝐹𝑥) ≠ ∅} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)}
6261a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → {𝑥𝐴 ∣ (𝐹𝑥) ≠ ∅} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
6359, 56, 623eqtr3d 2785 . . . . . . . . . . . . . 14 (𝜑 → {𝑥𝐴 ∣ (𝐹𝑥) ∈ (V ∖ {∅})} = {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)})
64 df-rab 3437 . . . . . . . . . . . . . . . 16 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
65 19.42v 1953 . . . . . . . . . . . . . . . . 17 (∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥)) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥)))
6665abbii 2809 . . . . . . . . . . . . . . . 16 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹𝑥))}
6764, 66eqtr4i 2768 . . . . . . . . . . . . . . 15 {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))}
6867a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑥𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹𝑥)} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))})
6956, 63, 683eqtrd 2781 . . . . . . . . . . . . 13 (𝜑 → (𝐹 supp ∅) = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 ∈ (𝐹𝑥))})
7045, 69eqtr4d 2780 . . . . . . . . . . . 12 (𝜑 → dom 𝑅 = (𝐹 supp ∅))
7170eleq1d 2826 . . . . . . . . . . 11 (𝜑 → (dom 𝑅 ∈ Fin ↔ (𝐹 supp ∅) ∈ Fin))
7271biimpa 476 . . . . . . . . . 10 ((𝜑 ∧ dom 𝑅 ∈ Fin) → (𝐹 supp ∅) ∈ Fin)
7337, 41, 43, 72ffsrn 32740 . . . . . . . . 9 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ran 𝐹 ∈ Fin)
7435, 73eqeltrrd 2842 . . . . . . . 8 ((𝜑 ∧ dom 𝑅 ∈ Fin) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin)
75 unifi 9384 . . . . . . . . 9 (({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin ∧ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin)
7675ex 412 . . . . . . . 8 ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin))
7774, 76syl 17 . . . . . . 7 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin))
78 unifi3 32724 . . . . . . 7 ( {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin)
7977, 78impbid1 225 . . . . . 6 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin ↔ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ∈ Fin))
8030, 79bitr4d 282 . . . . 5 ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ∈ Fin ↔ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin))
81 opabrn 32624 . . . . . . . 8 (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝐹𝑥))} → ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))})
821, 81syl 17 . . . . . . 7 (𝜑 → ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))})
8382eleq1d 2826 . . . . . 6 (𝜑 → (ran 𝑅 ∈ Fin ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ∈ Fin))
8483adantr 480 . . . . 5 ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝑅 ∈ Fin ↔ {𝑦 ∣ ∃𝑥(𝑥𝐴𝑦 ∈ (𝐹𝑥))} ∈ Fin))
8535sseq1d 4015 . . . . 5 ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝐹 ⊆ Fin ↔ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹𝑥)} ⊆ Fin))
8680, 84, 853bitr4d 311 . . . 4 ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝑅 ∈ Fin ↔ ran 𝐹 ⊆ Fin))
8786pm5.32da 579 . . 3 (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin) ↔ (dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin)))
8871anbi1d 631 . . 3 (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ ((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin)))
8987, 88bitrd 279 . 2 (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin) ↔ ((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin)))
90 ancom 460 . . 3 (((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin))
9190a1i 11 . 2 (𝜑 → (((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin)))
926, 89, 913bitrd 305 1 (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wne 2940  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626   cuni 4907  {copab 5205  cmpt 5225  ccnv 5684  dom cdm 5685  ran crn 5686  cima 5688  Rel wrel 5690  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431   supp csupp 8185  Fincfn 8985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-ac2 10503
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-fin 8989  df-card 9979  df-acn 9982  df-ac 10156
This theorem is referenced by:  fpwrelmapffs  32745
  Copyright terms: Public domain W3C validator