Step | Hyp | Ref
| Expression |
1 | | fpwrelmapffslem.4 |
. . 3
⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
2 | | relopab 5247 |
. . . 4
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
3 | | releq 5201 |
. . . 4
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → (Rel 𝑅 ↔ Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))})) |
4 | 2, 3 | mpbiri 248 |
. . 3
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → Rel 𝑅) |
5 | | relfi 29415 |
. . 3
⊢ (Rel
𝑅 → (𝑅 ∈ Fin ↔ (dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin))) |
6 | 1, 4, 5 | 3syl 18 |
. 2
⊢ (𝜑 → (𝑅 ∈ Fin ↔ (dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin))) |
7 | | rexcom4 3225 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥))) |
8 | | ancom 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ↔ (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥))) |
9 | 8 | exbii 1774 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥))) |
10 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑥) ∈ V |
11 | | eleq2 2690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑥) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐹‘𝑥))) |
12 | 10, 11 | ceqsexv 3242 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ↔ 𝑤 ∈ (𝐹‘𝑥)) |
13 | 9, 12 | bitr3i 266 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ 𝑤 ∈ (𝐹‘𝑥)) |
14 | 13 | rexbii 3041 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ (𝐹‘𝑥)) |
15 | | r19.42v 3092 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) |
16 | 15 | exbii 1774 |
. . . . . . . . . . . . 13
⊢
(∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) |
17 | 7, 14, 16 | 3bitr3ri 291 |
. . . . . . . . . . . 12
⊢
(∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ (𝐹‘𝑥)) |
18 | | df-rex 2918 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥))) |
19 | 17, 18 | bitr2i 265 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) |
20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)))) |
21 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
22 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑥))) |
23 | 22 | anbi2d 740 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)))) |
24 | 23 | exbidv 1850 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)))) |
25 | 21, 24 | elab 3350 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥))) |
26 | | eluniab 4447 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) |
27 | 20, 25, 26 | 3bitr4g 303 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ↔ 𝑤 ∈ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)})) |
28 | 27 | eqrdv 2620 |
. . . . . . . 8
⊢ (𝜑 → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) |
29 | 28 | eleq1d 2686 |
. . . . . . 7
⊢ (𝜑 → ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin ↔ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin ↔ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) |
31 | | fpwrelmapffslem.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵) |
32 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝒫 𝐵 → 𝐹 Fn 𝐴) |
33 | | fnrnfv 6242 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) |
34 | 31, 32, 33 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) |
35 | 34 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) |
36 | | 0ex 4790 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ∅ ∈
V) |
38 | | fpwrelmapffslem.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ V |
39 | | fex 6490 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝒫 𝐵 ∧ 𝐴 ∈ V) → 𝐹 ∈ V) |
40 | 31, 38, 39 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
41 | 40 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → 𝐹 ∈ V) |
42 | | ffun 6048 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝒫 𝐵 → Fun 𝐹) |
43 | 31, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → Fun 𝐹) |
45 | | opabdm 29423 |
. . . . . . . . . . . . . 14
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → dom 𝑅 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
46 | 1, 45 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝑅 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
47 | 38, 39 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝒫 𝐵 → 𝐹 ∈ V) |
48 | | suppimacnv 7306 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ V ∧ ∅ ∈
V) → (𝐹 supp ∅)
= (◡𝐹 “ (V ∖
{∅}))) |
49 | 36, 48 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ V → (𝐹 supp ∅) = (◡𝐹 “ (V ∖
{∅}))) |
50 | 31, 47, 49 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 supp ∅) = (◡𝐹 “ (V ∖
{∅}))) |
51 | 31 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
52 | 51 | cnveqd 5298 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝐹 = ◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
53 | 52 | imaeq1d 5465 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝐹 “ (V ∖ {∅})) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ (V ∖
{∅}))) |
54 | 50, 53 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ (V ∖
{∅}))) |
55 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) |
56 | 55 | mptpreima 5628 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ (V ∖ {∅})) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ (V ∖
{∅})} |
57 | 54, 56 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ (V ∖
{∅})}) |
58 | | suppvalfn 7302 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ ∅ ∈ V) →
(𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅}) |
59 | 38, 36, 58 | mp3an23 1416 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn 𝐴 → (𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅}) |
60 | 31, 32, 59 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅}) |
61 | | n0 3931 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))) |
63 | 62 | rabbiia 3185 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) |
65 | 60, 57, 64 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ (V ∖ {∅})} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) |
66 | | df-rab 2921 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
67 | | 19.42v 1918 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))) |
68 | 67 | abbii 2739 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} |
69 | 66, 68 | eqtr4i 2647 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
71 | 57, 65, 70 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp ∅) = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
72 | 46, 71 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝑅 = (𝐹 supp ∅)) |
73 | 72 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝜑 → (dom 𝑅 ∈ Fin ↔ (𝐹 supp ∅) ∈ Fin)) |
74 | 73 | biimpa 501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (𝐹 supp ∅) ∈ Fin) |
75 | 37, 41, 44, 74 | ffsrn 29504 |
. . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ran 𝐹 ∈ Fin) |
76 | 35, 75 | eqeltrrd 2702 |
. . . . . . . 8
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin) |
77 | | unifi 8255 |
. . . . . . . . 9
⊢ (({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin ∧ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin) → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin) |
78 | 77 | ex 450 |
. . . . . . . 8
⊢ ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) |
79 | 76, 78 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) |
80 | | unifi3 29490 |
. . . . . . 7
⊢ (∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin) |
81 | 79, 80 | impbid1 215 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin ↔ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) |
82 | 30, 81 | bitr4d 271 |
. . . . 5
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin ↔ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin)) |
83 | | opabrn 29424 |
. . . . . . . 8
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
84 | 1, 83 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) |
85 | 84 | eleq1d 2686 |
. . . . . 6
⊢ (𝜑 → (ran 𝑅 ∈ Fin ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin)) |
86 | 85 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝑅 ∈ Fin ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin)) |
87 | 35 | sseq1d 3632 |
. . . . 5
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝐹 ⊆ Fin ↔ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin)) |
88 | 82, 86, 87 | 3bitr4d 300 |
. . . 4
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝑅 ∈ Fin ↔ ran 𝐹 ⊆ Fin)) |
89 | 88 | pm5.32da 673 |
. . 3
⊢ (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin) ↔ (dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin))) |
90 | 73 | anbi1d 741 |
. . 3
⊢ (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ ((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin))) |
91 | 89, 90 | bitrd 268 |
. 2
⊢ (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin) ↔ ((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin))) |
92 | | ancom 466 |
. . 3
⊢ (((𝐹 supp ∅) ∈ Fin ∧
ran 𝐹 ⊆ Fin) ↔
(ran 𝐹 ⊆ Fin ∧
(𝐹 supp ∅) ∈
Fin)) |
93 | 92 | a1i 11 |
. 2
⊢ (𝜑 → (((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈
Fin))) |
94 | 6, 91, 93 | 3bitrd 294 |
1
⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈
Fin))) |