Step | Hyp | Ref
| Expression |
1 | | n0snor2el 4834 |
. 2
⊢ (𝐴 ≠ ∅ →
(∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧})) |
2 | | nfiu1 5031 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} |
3 | 2 | nfeq1 2918 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ |
4 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑥∃𝑧 𝐴 = {𝑧} |
5 | 3, 4 | nfim 1899 |
. . . 4
⊢
Ⅎ𝑥(∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}) |
6 | | ssiun2 5050 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → {⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) |
7 | | nfcv 2903 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑦 |
8 | | nfcsb1v 3918 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
9 | 7, 8 | nfop 4889 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩ |
10 | 9 | nfsn 4711 |
. . . . . . . . 9
⊢
Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} |
11 | 10, 2 | nfss 3974 |
. . . . . . . 8
⊢
Ⅎ𝑥{⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} |
12 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
13 | | csbeq1a 3907 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
14 | 12, 13 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝐵⟩ = ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩) |
15 | 14 | sneqd 4640 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {⟨𝑥, 𝐵⟩} = {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) |
16 | 15 | sseq1d 4013 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})) |
17 | 7, 11, 16, 6 | vtoclgaf 3564 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) |
18 | 6, 17 | anim12i 613 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩})) |
19 | | unss 4184 |
. . . . . . 7
⊢
(({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) |
20 | | sseq2 4008 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ↔ ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩)) |
21 | | df-pr 4631 |
. . . . . . . . . . . 12
⊢
{⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} = ({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) |
22 | 21 | eqcomi 2741 |
. . . . . . . . . . 11
⊢
({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) = {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} |
23 | 22 | sseq1i 4010 |
. . . . . . . . . 10
⊢
(({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ ↔ {⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩) |
24 | | vex 3478 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
25 | | iunopeqop.b |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
26 | | vex 3478 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
27 | 25 | csbex 5311 |
. . . . . . . . . . . 12
⊢
⦋𝑦 /
𝑥⦌𝐵 ∈ V |
28 | | iunopeqop.c |
. . . . . . . . . . . 12
⊢ 𝐶 ∈ V |
29 | | iunopeqop.d |
. . . . . . . . . . . 12
⊢ 𝐷 ∈ V |
30 | 24, 25, 26, 27, 28, 29 | propssopi 5508 |
. . . . . . . . . . 11
⊢
({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → 𝑥 = 𝑦) |
31 | | eqneqall 2951 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢
({⟨𝑥, 𝐵⟩, ⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))) |
33 | 23, 32 | sylbi 216 |
. . . . . . . . 9
⊢
(({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ⟨𝐶, 𝐷⟩ → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧}))) |
34 | 20, 33 | syl6bi 252 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 𝐴 = {𝑧})))) |
35 | 34 | com14 96 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ∪ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩}) ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} → (𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))) |
36 | 19, 35 | biimtrid 241 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (({⟨𝑥, 𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} ∧ {⟨𝑦, ⦋𝑦 / 𝑥⦌𝐵⟩} ⊆ ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) → (𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})))) |
37 | 18, 36 | mpd 15 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))) |
38 | 37 | rexlimdva 3155 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))) |
39 | 5, 38 | rexlimi 3256 |
. . 3
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → (∪
𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})) |
40 | | ax-1 6 |
. . 3
⊢
(∃𝑧 𝐴 = {𝑧} → (∪
𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})) |
41 | 39, 40 | jaoi 855 |
. 2
⊢
((∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}) → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})) |
42 | 1, 41 | syl 17 |
1
⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})) |