Proof of Theorem aciunf1
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3993 |
. . . 4
⊢ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ⊆ 𝐴 |
2 | | aciunf1.0 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | ssexg 5216 |
. . . 4
⊢ (({𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ∈ V) |
4 | 1, 2, 3 | sylancr 590 |
. . 3
⊢ (𝜑 → {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ∈ V) |
5 | | rabid 3290 |
. . . . . 6
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ↔ (𝑗 ∈ 𝐴 ∧ 𝐵 ≠ ∅)) |
6 | 5 | biimpi 219 |
. . . . 5
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} → (𝑗 ∈ 𝐴 ∧ 𝐵 ≠ ∅)) |
7 | 6 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}) → (𝑗 ∈ 𝐴 ∧ 𝐵 ≠ ∅)) |
8 | 7 | simprd 499 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}) → 𝐵 ≠ ∅) |
9 | | nfrab1 3296 |
. . 3
⊢
Ⅎ𝑗{𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} |
10 | 7 | simpld 498 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}) → 𝑗 ∈ 𝐴) |
11 | | aciunf1.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
12 | 10, 11 | syldan 594 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}) → 𝐵 ∈ 𝑊) |
13 | 4, 8, 9, 12 | aciunf1lem 30719 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵–1-1→∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪
𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) |
14 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → 𝑓 = 𝑓) |
15 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
16 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑗𝐴 |
17 | | nfrab1 3296 |
. . . . . . . 8
⊢
Ⅎ𝑗{𝑗 ∈ 𝐴 ∣ 𝐵 = ∅} |
18 | 16, 17 | nfdif 4040 |
. . . . . . 7
⊢
Ⅎ𝑗(𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) |
19 | | difrab 4223 |
. . . . . . . . 9
⊢ ({𝑗 ∈ 𝐴 ∣ ⊤} ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) = {𝑗 ∈ 𝐴 ∣ (⊤ ∧ ¬ 𝐵 = ∅)} |
20 | 16 | rabtru 3599 |
. . . . . . . . . 10
⊢ {𝑗 ∈ 𝐴 ∣ ⊤} = 𝐴 |
21 | 20 | difeq1i 4033 |
. . . . . . . . 9
⊢ ({𝑗 ∈ 𝐴 ∣ ⊤} ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) = (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) |
22 | | truan 1554 |
. . . . . . . . . . 11
⊢
((⊤ ∧ ¬ 𝐵 = ∅) ↔ ¬ 𝐵 = ∅) |
23 | | df-ne 2941 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅) |
24 | 22, 23 | bitr4i 281 |
. . . . . . . . . 10
⊢
((⊤ ∧ ¬ 𝐵 = ∅) ↔ 𝐵 ≠ ∅) |
25 | 24 | rabbii 3383 |
. . . . . . . . 9
⊢ {𝑗 ∈ 𝐴 ∣ (⊤ ∧ ¬ 𝐵 = ∅)} = {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} |
26 | 19, 21, 25 | 3eqtr3i 2773 |
. . . . . . . 8
⊢ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) = {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) = {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}) |
28 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = 𝐵) |
29 | 15, 18, 9, 27, 28 | iuneq12df 4930 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅})𝐵 = ∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵) |
30 | | rabid 3290 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅} ↔ (𝑗 ∈ 𝐴 ∧ 𝐵 = ∅)) |
31 | 30 | biimpi 219 |
. . . . . . . . . 10
⊢ (𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅} → (𝑗 ∈ 𝐴 ∧ 𝐵 = ∅)) |
32 | 31 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) → (𝑗 ∈ 𝐴 ∧ 𝐵 = ∅)) |
33 | 32 | simprd 499 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝐵 = ∅) |
34 | 33 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}𝐵 = ∅) |
35 | 17 | iunxdif3 5003 |
. . . . . . 7
⊢
(∀𝑗 ∈
{𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}𝐵 = ∅ → ∪ 𝑗 ∈ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅})𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅})𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵) |
37 | 29, 36 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵) |
38 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → ({𝑗} × 𝐵) = ({𝑗} × 𝐵)) |
39 | 15, 18, 9, 27, 38 | iuneq12df 4930 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅})({𝑗} × 𝐵) = ∪
𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ({𝑗} × 𝐵)) |
40 | 33 | xpeq2d 5581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) → ({𝑗} × 𝐵) = ({𝑗} × ∅)) |
41 | | xp0 6021 |
. . . . . . . . 9
⊢ ({𝑗} × ∅) =
∅ |
42 | 40, 41 | eqtrdi 2794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅}) → ({𝑗} × 𝐵) = ∅) |
43 | 42 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅} ({𝑗} × 𝐵) = ∅) |
44 | 17 | iunxdif3 5003 |
. . . . . . 7
⊢
(∀𝑗 ∈
{𝑗 ∈ 𝐴 ∣ 𝐵 = ∅} ({𝑗} × 𝐵) = ∅ → ∪ 𝑗 ∈ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅})({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ (𝐴 ∖ {𝑗 ∈ 𝐴 ∣ 𝐵 = ∅})({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
46 | 39, 45 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
47 | 14, 37, 46 | f1eq123d 6653 |
. . . 4
⊢ (𝜑 → (𝑓:∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵–1-1→∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ({𝑗} × 𝐵) ↔ 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
48 | 37 | raleqdv 3325 |
. . . 4
⊢ (𝜑 → (∀𝑘 ∈ ∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘 ↔ ∀𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) |
49 | 47, 48 | anbi12d 634 |
. . 3
⊢ (𝜑 → ((𝑓:∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵–1-1→∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪
𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘) ↔ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘))) |
50 | 49 | exbidv 1929 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵–1-1→∪ 𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅} ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪
𝑗 ∈ {𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅}𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘) ↔ ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘))) |
51 | 13, 50 | mpbid 235 |
1
⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) |