Step | Hyp | Ref
| Expression |
1 | | ixpsnf1o.f |
. 2
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) |
2 | | snex 5333 |
. . . 4
⊢ {𝐼} ∈ V |
3 | | snex 5333 |
. . . 4
⊢ {𝑥} ∈ V |
4 | 2, 3 | xpex 7547 |
. . 3
⊢ ({𝐼} × {𝑥}) ∈ V |
5 | 4 | a1i 11 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → ({𝐼} × {𝑥}) ∈ V) |
6 | | vex 3419 |
. . . . 5
⊢ 𝑎 ∈ V |
7 | 6 | rnex 7699 |
. . . 4
⊢ ran 𝑎 ∈ V |
8 | 7 | uniex 7538 |
. . 3
⊢ ∪ ran 𝑎 ∈ V |
9 | 8 | a1i 11 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑎 ∈ X𝑦 ∈ {𝐼}𝐴) → ∪ ran
𝑎 ∈
V) |
10 | | sneq 4560 |
. . . . . 6
⊢ (𝑏 = 𝐼 → {𝑏} = {𝐼}) |
11 | 10 | xpeq1d 5589 |
. . . . 5
⊢ (𝑏 = 𝐼 → ({𝑏} × {𝑥}) = ({𝐼} × {𝑥})) |
12 | 11 | eqeq2d 2749 |
. . . 4
⊢ (𝑏 = 𝐼 → (𝑎 = ({𝑏} × {𝑥}) ↔ 𝑎 = ({𝐼} × {𝑥}))) |
13 | 12 | anbi2d 632 |
. . 3
⊢ (𝑏 = 𝐼 → ((𝑥 ∈ 𝐴 ∧ 𝑎 = ({𝑏} × {𝑥})) ↔ (𝑥 ∈ 𝐴 ∧ 𝑎 = ({𝐼} × {𝑥})))) |
14 | | elixpsn 8627 |
. . . . . 6
⊢ (𝑏 ∈ V → (𝑎 ∈ X𝑦 ∈
{𝑏}𝐴 ↔ ∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉})) |
15 | 14 | elv 3421 |
. . . . 5
⊢ (𝑎 ∈ X𝑦 ∈
{𝑏}𝐴 ↔ ∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉}) |
16 | 10 | ixpeq1d 8599 |
. . . . . 6
⊢ (𝑏 = 𝐼 → X𝑦 ∈ {𝑏}𝐴 = X𝑦 ∈ {𝐼}𝐴) |
17 | 16 | eleq2d 2824 |
. . . . 5
⊢ (𝑏 = 𝐼 → (𝑎 ∈ X𝑦 ∈ {𝑏}𝐴 ↔ 𝑎 ∈ X𝑦 ∈ {𝐼}𝐴)) |
18 | 15, 17 | bitr3id 288 |
. . . 4
⊢ (𝑏 = 𝐼 → (∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ↔ 𝑎 ∈ X𝑦 ∈ {𝐼}𝐴)) |
19 | 18 | anbi1d 633 |
. . 3
⊢ (𝑏 = 𝐼 → ((∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎) ↔ (𝑎 ∈ X𝑦 ∈ {𝐼}𝐴 ∧ 𝑥 = ∪ ran 𝑎))) |
20 | | vex 3419 |
. . . . . . 7
⊢ 𝑏 ∈ V |
21 | | vex 3419 |
. . . . . . 7
⊢ 𝑥 ∈ V |
22 | 20, 21 | xpsn 6965 |
. . . . . 6
⊢ ({𝑏} × {𝑥}) = {〈𝑏, 𝑥〉} |
23 | 22 | eqeq2i 2751 |
. . . . 5
⊢ (𝑎 = ({𝑏} × {𝑥}) ↔ 𝑎 = {〈𝑏, 𝑥〉}) |
24 | 23 | anbi2i 626 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑎 = ({𝑏} × {𝑥})) ↔ (𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉})) |
25 | | eqid 2738 |
. . . . . . . . 9
⊢
{〈𝑏, 𝑥〉} = {〈𝑏, 𝑥〉} |
26 | | opeq2 4794 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑥 → 〈𝑏, 𝑐〉 = 〈𝑏, 𝑥〉) |
27 | 26 | sneqd 4562 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉}) |
28 | 27 | rspceeqv 3559 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ {〈𝑏, 𝑥〉} = {〈𝑏, 𝑥〉}) → ∃𝑐 ∈ 𝐴 {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉}) |
29 | 25, 28 | mpan2 691 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → ∃𝑐 ∈ 𝐴 {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉}) |
30 | 20, 21 | op2nda 6100 |
. . . . . . . . 9
⊢ ∪ ran {〈𝑏, 𝑥〉} = 𝑥 |
31 | 30 | eqcomi 2747 |
. . . . . . . 8
⊢ 𝑥 = ∪
ran {〈𝑏, 𝑥〉} |
32 | 29, 31 | jctir 524 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (∃𝑐 ∈ 𝐴 {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran
{〈𝑏, 𝑥〉})) |
33 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑎 = {〈𝑏, 𝑥〉} → (𝑎 = {〈𝑏, 𝑐〉} ↔ {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉})) |
34 | 33 | rexbidv 3223 |
. . . . . . . 8
⊢ (𝑎 = {〈𝑏, 𝑥〉} → (∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ↔ ∃𝑐 ∈ 𝐴 {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉})) |
35 | | rneq 5814 |
. . . . . . . . . 10
⊢ (𝑎 = {〈𝑏, 𝑥〉} → ran 𝑎 = ran {〈𝑏, 𝑥〉}) |
36 | 35 | unieqd 4842 |
. . . . . . . . 9
⊢ (𝑎 = {〈𝑏, 𝑥〉} → ∪
ran 𝑎 = ∪ ran {〈𝑏, 𝑥〉}) |
37 | 36 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑎 = {〈𝑏, 𝑥〉} → (𝑥 = ∪ ran 𝑎 ↔ 𝑥 = ∪ ran
{〈𝑏, 𝑥〉})) |
38 | 34, 37 | anbi12d 634 |
. . . . . . 7
⊢ (𝑎 = {〈𝑏, 𝑥〉} → ((∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎) ↔ (∃𝑐 ∈ 𝐴 {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran
{〈𝑏, 𝑥〉}))) |
39 | 32, 38 | syl5ibrcom 250 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → (𝑎 = {〈𝑏, 𝑥〉} → (∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎))) |
40 | 39 | imp 410 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉}) → (∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎)) |
41 | | vex 3419 |
. . . . . . . . . . 11
⊢ 𝑐 ∈ V |
42 | 20, 41 | op2nda 6100 |
. . . . . . . . . 10
⊢ ∪ ran {〈𝑏, 𝑐〉} = 𝑐 |
43 | 42 | eqeq2i 2751 |
. . . . . . . . 9
⊢ (𝑥 = ∪
ran {〈𝑏, 𝑐〉} ↔ 𝑥 = 𝑐) |
44 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝐴 → {〈𝑏, 𝑐〉} = {〈𝑏, 𝑐〉}) |
45 | 44 | ancli 552 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝐴 → (𝑐 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑐〉})) |
46 | | eleq1w 2821 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑐 → (𝑥 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴)) |
47 | | opeq2 4794 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑐 → 〈𝑏, 𝑥〉 = 〈𝑏, 𝑐〉) |
48 | 47 | sneqd 4562 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑐 → {〈𝑏, 𝑥〉} = {〈𝑏, 𝑐〉}) |
49 | 48 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑐 → ({〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉} ↔ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑐〉})) |
50 | 46, 49 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑐 → ((𝑥 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉}) ↔ (𝑐 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑐〉}))) |
51 | 45, 50 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝑐 ∈ 𝐴 → (𝑥 = 𝑐 → (𝑥 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉}))) |
52 | 43, 51 | syl5bi 245 |
. . . . . . . 8
⊢ (𝑐 ∈ 𝐴 → (𝑥 = ∪ ran
{〈𝑏, 𝑐〉} → (𝑥 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉}))) |
53 | | rneq 5814 |
. . . . . . . . . . 11
⊢ (𝑎 = {〈𝑏, 𝑐〉} → ran 𝑎 = ran {〈𝑏, 𝑐〉}) |
54 | 53 | unieqd 4842 |
. . . . . . . . . 10
⊢ (𝑎 = {〈𝑏, 𝑐〉} → ∪
ran 𝑎 = ∪ ran {〈𝑏, 𝑐〉}) |
55 | 54 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑎 = {〈𝑏, 𝑐〉} → (𝑥 = ∪ ran 𝑎 ↔ 𝑥 = ∪ ran
{〈𝑏, 𝑐〉})) |
56 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝑎 = {〈𝑏, 𝑐〉} → (𝑎 = {〈𝑏, 𝑥〉} ↔ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉})) |
57 | 56 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑎 = {〈𝑏, 𝑐〉} → ((𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉}) ↔ (𝑥 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉}))) |
58 | 55, 57 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑎 = {〈𝑏, 𝑐〉} → ((𝑥 = ∪ ran 𝑎 → (𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉})) ↔ (𝑥 = ∪ ran
{〈𝑏, 𝑐〉} → (𝑥 ∈ 𝐴 ∧ {〈𝑏, 𝑐〉} = {〈𝑏, 𝑥〉})))) |
59 | 52, 58 | syl5ibrcom 250 |
. . . . . . 7
⊢ (𝑐 ∈ 𝐴 → (𝑎 = {〈𝑏, 𝑐〉} → (𝑥 = ∪ ran 𝑎 → (𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉})))) |
60 | 59 | rexlimiv 3206 |
. . . . . 6
⊢
(∃𝑐 ∈
𝐴 𝑎 = {〈𝑏, 𝑐〉} → (𝑥 = ∪ ran 𝑎 → (𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉}))) |
61 | 60 | imp 410 |
. . . . 5
⊢
((∃𝑐 ∈
𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎) → (𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉})) |
62 | 40, 61 | impbii 212 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑎 = {〈𝑏, 𝑥〉}) ↔ (∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎)) |
63 | 24, 62 | bitri 278 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑎 = ({𝑏} × {𝑥})) ↔ (∃𝑐 ∈ 𝐴 𝑎 = {〈𝑏, 𝑐〉} ∧ 𝑥 = ∪ ran 𝑎)) |
64 | 13, 19, 63 | vtoclbg 3490 |
. 2
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ∧ 𝑎 = ({𝐼} × {𝑥})) ↔ (𝑎 ∈ X𝑦 ∈ {𝐼}𝐴 ∧ 𝑥 = ∪ ran 𝑎))) |
65 | 1, 5, 9, 64 | f1od 7466 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐹:𝐴–1-1-onto→X𝑦 ∈
{𝐼}𝐴) |