Proof of Theorem ralxpmap
Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . 3
⊢ 𝑔 ∈ V |
2 | | snex 4835 |
. . 3
⊢
{〈𝐽, 𝑦〉} ∈
V |
3 | 1, 2 | unex 6854 |
. 2
⊢ (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ V |
4 | | simpr 476 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) |
5 | | elmapex 7764 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑆 ↑𝑚 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
7 | | elmapg 7757 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑓 ∈ (𝑆 ↑𝑚 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → (𝑓 ∈ (𝑆 ↑𝑚 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
9 | 4, 8 | mpbid 221 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝑓:𝑇⟶𝑆) |
10 | | simpl 472 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝐽 ∈ 𝑇) |
11 | 9, 10 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → (𝑓‘𝐽) ∈ 𝑆) |
12 | | difss 3699 |
. . . . . . 7
⊢ (𝑇 ∖ {𝐽}) ⊆ 𝑇 |
13 | | fssres 5983 |
. . . . . . 7
⊢ ((𝑓:𝑇⟶𝑆 ∧ (𝑇 ∖ {𝐽}) ⊆ 𝑇) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
14 | 9, 12, 13 | sylancl 693 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
15 | 5 | simpld 474 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑆 ↑𝑚 𝑇) → 𝑆 ∈ V) |
16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝑆 ∈ V) |
17 | 6 | simprd 478 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝑇 ∈ V) |
18 | | difexg 4735 |
. . . . . . . 8
⊢ (𝑇 ∈ V → (𝑇 ∖ {𝐽}) ∈ V) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → (𝑇 ∖ {𝐽}) ∈ V) |
20 | 16, 19 | elmapd 7758 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})) ↔ (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆)) |
21 | 14, 20 | mpbird 246 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))) |
22 | | ffn 5958 |
. . . . . . 7
⊢ (𝑓:𝑇⟶𝑆 → 𝑓 Fn 𝑇) |
23 | 9, 22 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝑓 Fn 𝑇) |
24 | | fnsnsplit 6355 |
. . . . . 6
⊢ ((𝑓 Fn 𝑇 ∧ 𝐽 ∈ 𝑇) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
25 | 23, 10, 24 | syl2anc 691 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
26 | | opeq2 4341 |
. . . . . . . . 9
⊢ (𝑦 = (𝑓‘𝐽) → 〈𝐽, 𝑦〉 = 〈𝐽, (𝑓‘𝐽)〉) |
27 | 26 | sneqd 4137 |
. . . . . . . 8
⊢ (𝑦 = (𝑓‘𝐽) → {〈𝐽, 𝑦〉} = {〈𝐽, (𝑓‘𝐽)〉}) |
28 | 27 | uneq2d 3729 |
. . . . . . 7
⊢ (𝑦 = (𝑓‘𝐽) → (𝑔 ∪ {〈𝐽, 𝑦〉}) = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
29 | 28 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝐽) → (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) ↔ 𝑓 = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}))) |
30 | | uneq1 3722 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}) = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
31 | 30 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑓 = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}) ↔ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉}))) |
32 | 29, 31 | rspc2ev 3295 |
. . . . 5
⊢ (((𝑓‘𝐽) ∈ 𝑆 ∧ (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})) ∧ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) |
33 | 11, 21, 25, 32 | syl3anc 1318 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑𝑚 𝑇)) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) |
34 | 33 | ex 449 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑𝑚 𝑇) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}))) |
35 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
36 | 35 | ad2antll 761 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
37 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
38 | | f1osng 6089 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {〈𝐽, 𝑦〉}:{𝐽}–1-1-onto→{𝑦}) |
39 | | f1of 6050 |
. . . . . . . . . . . 12
⊢
({〈𝐽, 𝑦〉}:{𝐽}–1-1-onto→{𝑦} → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
41 | 37, 40 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝐽 ∈ 𝑇 → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
43 | | incom 3767 |
. . . . . . . . . . 11
⊢ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ({𝐽} ∩ (𝑇 ∖ {𝐽})) |
44 | | disjdif 3992 |
. . . . . . . . . . 11
⊢ ({𝐽} ∩ (𝑇 ∖ {𝐽})) = ∅ |
45 | 43, 44 | eqtri 2632 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅ |
46 | 45 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) |
47 | | fun 5979 |
. . . . . . . . 9
⊢ (((𝑔:(𝑇 ∖ {𝐽})⟶𝑆 ∧ {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) ∧ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) → (𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
48 | 36, 42, 46, 47 | syl21anc 1317 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
49 | | uncom 3719 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = ({𝐽} ∪ (𝑇 ∖ {𝐽})) |
50 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → 𝐽 ∈ 𝑇) |
51 | 50 | snssd 4281 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → {𝐽} ⊆ 𝑇) |
52 | | undif 4001 |
. . . . . . . . . . 11
⊢ ({𝐽} ⊆ 𝑇 ↔ ({𝐽} ∪ (𝑇 ∖ {𝐽})) = 𝑇) |
53 | 51, 52 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → ({𝐽} ∪ (𝑇 ∖ {𝐽})) = 𝑇) |
54 | 49, 53 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = 𝑇) |
55 | 54 | feq2d 5944 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦}) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶(𝑆 ∪ {𝑦}))) |
56 | 48, 55 | mpbid 221 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶(𝑆 ∪ {𝑦})) |
57 | | ssid 3587 |
. . . . . . . . 9
⊢ 𝑆 ⊆ 𝑆 |
58 | 57 | a1i 11 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → 𝑆 ⊆ 𝑆) |
59 | | snssi 4280 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 → {𝑦} ⊆ 𝑆) |
60 | 59 | ad2antrl 760 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → {𝑦} ⊆ 𝑆) |
61 | 58, 60 | unssd 3751 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑆 ∪ {𝑦}) ⊆ 𝑆) |
62 | 56, 61 | fssd 5970 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶𝑆) |
63 | | elmapex 7764 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
64 | 63 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
65 | 64 | simpld 474 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → 𝑆 ∈ V) |
66 | | ssun1 3738 |
. . . . . . . 8
⊢ 𝑇 ⊆ (𝑇 ∪ {𝐽}) |
67 | | undif1 3995 |
. . . . . . . . 9
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = (𝑇 ∪ {𝐽}) |
68 | 64 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑇 ∖ {𝐽}) ∈ V) |
69 | | snex 4835 |
. . . . . . . . . 10
⊢ {𝐽} ∈ V |
70 | | unexg 6857 |
. . . . . . . . . 10
⊢ (((𝑇 ∖ {𝐽}) ∈ V ∧ {𝐽} ∈ V) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
71 | 68, 69, 70 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
72 | 67, 71 | syl5eqelr 2693 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑇 ∪ {𝐽}) ∈ V) |
73 | | ssexg 4732 |
. . . . . . . 8
⊢ ((𝑇 ⊆ (𝑇 ∪ {𝐽}) ∧ (𝑇 ∪ {𝐽}) ∈ V) → 𝑇 ∈ V) |
74 | 66, 72, 73 | sylancr 694 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → 𝑇 ∈ V) |
75 | 65, 74 | elmapd 7758 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑𝑚 𝑇) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶𝑆)) |
76 | 62, 75 | mpbird 246 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑𝑚 𝑇)) |
77 | | eleq1 2676 |
. . . . 5
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝑓 ∈ (𝑆 ↑𝑚 𝑇) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑𝑚 𝑇))) |
78 | 76, 77 | syl5ibrcom 236 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽})))) → (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → 𝑓 ∈ (𝑆 ↑𝑚 𝑇))) |
79 | 78 | rexlimdvva 3020 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → 𝑓 ∈ (𝑆 ↑𝑚 𝑇))) |
80 | 34, 79 | impbid 201 |
. 2
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑𝑚 𝑇) ↔ ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}))) |
81 | | ralxpmap.j |
. . 3
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝜑 ↔ 𝜓)) |
82 | 81 | adantl 481 |
. 2
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) → (𝜑 ↔ 𝜓)) |
83 | 3, 80, 82 | ralxpxfr2d 3298 |
1
⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑𝑚 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝜓)) |