Step | Hyp | Ref
| Expression |
1 | | n0snor2el 4744 |
. 2
⊢ (𝐴 ≠ ∅ →
(∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧})) |
2 | | nfiu1 4938 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} |
3 | 2 | nfeq1 2919 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 |
4 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑥∃𝑧 𝐴 = {𝑧} |
5 | 3, 4 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑥(∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧}) |
6 | | ssiun2 4956 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → {〈𝑥, 𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) |
7 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑦 |
8 | | nfcsb1v 3836 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
9 | 7, 8 | nfop 4800 |
. . . . . . . . . 10
⊢
Ⅎ𝑥〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉 |
10 | 9 | nfsn 4623 |
. . . . . . . . 9
⊢
Ⅎ𝑥{〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} |
11 | 10, 2 | nfss 3892 |
. . . . . . . 8
⊢
Ⅎ𝑥{〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} |
12 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
13 | | csbeq1a 3825 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
14 | 12, 13 | opeq12d 4792 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝐵〉 = 〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉) |
15 | 14 | sneqd 4553 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {〈𝑥, 𝐵〉} = {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) |
16 | 15 | sseq1d 3932 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({〈𝑥, 𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} ↔ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉})) |
17 | 7, 11, 16, 6 | vtoclgaf 3488 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) |
18 | 6, 17 | anim12i 616 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ({〈𝑥, 𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} ∧ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉})) |
19 | | unss 4098 |
. . . . . . 7
⊢
(({〈𝑥, 𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} ∧ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) ↔ ({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) |
20 | | sseq2 3927 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → (({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} ↔ ({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ 〈𝐶, 𝐷〉)) |
21 | | df-pr 4544 |
. . . . . . . . . . . 12
⊢
{〈𝑥, 𝐵〉, 〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} = ({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) |
22 | 21 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) = {〈𝑥, 𝐵〉, 〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} |
23 | 22 | sseq1i 3929 |
. . . . . . . . . 10
⊢
(({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ 〈𝐶, 𝐷〉 ↔ {〈𝑥, 𝐵〉, 〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ 〈𝐶, 𝐷〉) |
24 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
25 | | iunopeqop.b |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
26 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
27 | 25 | csbex 5204 |
. . . . . . . . . . . 12
⊢
⦋𝑦 /
𝑥⦌𝐵 ∈ V |
28 | | iunopeqop.c |
. . . . . . . . . . . 12
⊢ 𝐶 ∈ V |
29 | | iunopeqop.d |
. . . . . . . . . . . 12
⊢ 𝐷 ∈ V |
30 | 24, 25, 26, 27, 28, 29 | propssopi 5391 |
. . . . . . . . . . 11
⊢
({〈𝑥, 𝐵〉, 〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ 〈𝐶, 𝐷〉 → 𝑥 = 𝑦) |
31 | | eqneqall 2951 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢
({〈𝑥, 𝐵〉, 〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ 〈𝐶, 𝐷〉 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))) |
33 | 23, 32 | sylbi 220 |
. . . . . . . . 9
⊢
(({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ 〈𝐶, 𝐷〉 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))) |
34 | 20, 33 | syl6bi 256 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → (({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))) |
35 | 34 | com14 96 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({〈𝑥, 𝐵〉} ∪ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉}) ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} → (𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})))) |
36 | 19, 35 | syl5bi 245 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({〈𝑥, 𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} ∧ {〈𝑦, ⦋𝑦 / 𝑥⦌𝐵〉} ⊆ ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) → (𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})))) |
37 | 18, 36 | mpd 15 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧}))) |
38 | 37 | rexlimdva 3203 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧}))) |
39 | 5, 38 | rexlimi 3234 |
. . 3
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})) |
40 | | ax-1 6 |
. . 3
⊢
(∃𝑧 𝐴 = {𝑧} → (∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})) |
41 | 39, 40 | jaoi 857 |
. 2
⊢
((∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}) → (∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})) |
42 | 1, 41 | syl 17 |
1
⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} = 〈𝐶, 𝐷〉 → ∃𝑧 𝐴 = {𝑧})) |