Proof of Theorem ralxpmap
Step | Hyp | Ref
| Expression |
1 | | vex 3500 |
. . 3
⊢ 𝑔 ∈ V |
2 | | snex 5335 |
. . 3
⊢
{〈𝐽, 𝑦〉} ∈
V |
3 | 1, 2 | unex 7472 |
. 2
⊢ (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ V |
4 | | simpr 487 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 ∈ (𝑆 ↑m 𝑇)) |
5 | | elmapex 8430 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑆 ↑m 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
6 | 5 | adantl 484 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
7 | | elmapg 8422 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
9 | 4, 8 | mpbid 234 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓:𝑇⟶𝑆) |
10 | | simpl 485 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝐽 ∈ 𝑇) |
11 | 9, 10 | ffvelrnd 6855 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓‘𝐽) ∈ 𝑆) |
12 | | difss 4111 |
. . . . . . 7
⊢ (𝑇 ∖ {𝐽}) ⊆ 𝑇 |
13 | | fssres 6547 |
. . . . . . 7
⊢ ((𝑓:𝑇⟶𝑆 ∧ (𝑇 ∖ {𝐽}) ⊆ 𝑇) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
14 | 9, 12, 13 | sylancl 588 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
15 | 5 | simpld 497 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑆 ↑m 𝑇) → 𝑆 ∈ V) |
16 | 15 | adantl 484 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑆 ∈ V) |
17 | 6 | simprd 498 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑇 ∈ V) |
18 | | difexg 5234 |
. . . . . . . 8
⊢ (𝑇 ∈ V → (𝑇 ∖ {𝐽}) ∈ V) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑇 ∖ {𝐽}) ∈ V) |
20 | 16, 19 | elmapd 8423 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) ↔ (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆)) |
21 | 14, 20 | mpbird 259 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))) |
22 | 9 | ffnd 6518 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 Fn 𝑇) |
23 | | fnsnsplit 6949 |
. . . . . 6
⊢ ((𝑓 Fn 𝑇 ∧ 𝐽 ∈ 𝑇) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
24 | 22, 10, 23 | syl2anc 586 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
25 | | opeq2 4807 |
. . . . . . . . 9
⊢ (𝑦 = (𝑓‘𝐽) → 〈𝐽, 𝑦〉 = 〈𝐽, (𝑓‘𝐽)〉) |
26 | 25 | sneqd 4582 |
. . . . . . . 8
⊢ (𝑦 = (𝑓‘𝐽) → {〈𝐽, 𝑦〉} = {〈𝐽, (𝑓‘𝐽)〉}) |
27 | 26 | uneq2d 4142 |
. . . . . . 7
⊢ (𝑦 = (𝑓‘𝐽) → (𝑔 ∪ {〈𝐽, 𝑦〉}) = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
28 | 27 | eqeq2d 2835 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝐽) → (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) ↔ 𝑓 = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}))) |
29 | | uneq1 4135 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}) = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
30 | 29 | eqeq2d 2835 |
. . . . . 6
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑓 = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}) ↔ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉}))) |
31 | 28, 30 | rspc2ev 3638 |
. . . . 5
⊢ (((𝑓‘𝐽) ∈ 𝑆 ∧ (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) ∧ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) |
32 | 11, 21, 24, 31 | syl3anc 1367 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) |
33 | 32 | ex 415 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑m 𝑇) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}))) |
34 | | elmapi 8431 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
35 | 34 | ad2antll 727 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
36 | | f1osng 6658 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {〈𝐽, 𝑦〉}:{𝐽}–1-1-onto→{𝑦}) |
37 | | f1of 6618 |
. . . . . . . . . . . 12
⊢
({〈𝐽, 𝑦〉}:{𝐽}–1-1-onto→{𝑦} → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
39 | 38 | elvd 3503 |
. . . . . . . . . 10
⊢ (𝐽 ∈ 𝑇 → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
40 | 39 | adantr 483 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
41 | | incom 4181 |
. . . . . . . . . . 11
⊢ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ({𝐽} ∩ (𝑇 ∖ {𝐽})) |
42 | | disjdif 4424 |
. . . . . . . . . . 11
⊢ ({𝐽} ∩ (𝑇 ∖ {𝐽})) = ∅ |
43 | 41, 42 | eqtri 2847 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅ |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) |
45 | | fun 6543 |
. . . . . . . . 9
⊢ (((𝑔:(𝑇 ∖ {𝐽})⟶𝑆 ∧ {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) ∧ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) → (𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
46 | 35, 40, 44, 45 | syl21anc 835 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
47 | | uncom 4132 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = ({𝐽} ∪ (𝑇 ∖ {𝐽})) |
48 | | simpl 485 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝐽 ∈ 𝑇) |
49 | 48 | snssd 4745 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {𝐽} ⊆ 𝑇) |
50 | | undif 4433 |
. . . . . . . . . . 11
⊢ ({𝐽} ⊆ 𝑇 ↔ ({𝐽} ∪ (𝑇 ∖ {𝐽})) = 𝑇) |
51 | 49, 50 | sylib 220 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ({𝐽} ∪ (𝑇 ∖ {𝐽})) = 𝑇) |
52 | 47, 51 | syl5eq 2871 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = 𝑇) |
53 | 52 | feq2d 6503 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦}) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶(𝑆 ∪ {𝑦}))) |
54 | 46, 53 | mpbid 234 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶(𝑆 ∪ {𝑦})) |
55 | | ssidd 3993 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑆 ⊆ 𝑆) |
56 | | snssi 4744 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 → {𝑦} ⊆ 𝑆) |
57 | 56 | ad2antrl 726 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {𝑦} ⊆ 𝑆) |
58 | 55, 57 | unssd 4165 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑆 ∪ {𝑦}) ⊆ 𝑆) |
59 | 54, 58 | fssd 6531 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶𝑆) |
60 | | elmapex 8430 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
61 | 60 | ad2antll 727 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
62 | 61 | simpld 497 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑆 ∈ V) |
63 | | ssun1 4151 |
. . . . . . . 8
⊢ 𝑇 ⊆ (𝑇 ∪ {𝐽}) |
64 | | undif1 4427 |
. . . . . . . . 9
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = (𝑇 ∪ {𝐽}) |
65 | 61 | simprd 498 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑇 ∖ {𝐽}) ∈ V) |
66 | | snex 5335 |
. . . . . . . . . 10
⊢ {𝐽} ∈ V |
67 | | unexg 7475 |
. . . . . . . . . 10
⊢ (((𝑇 ∖ {𝐽}) ∈ V ∧ {𝐽} ∈ V) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
68 | 65, 66, 67 | sylancl 588 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
69 | 64, 68 | eqeltrrid 2921 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑇 ∪ {𝐽}) ∈ V) |
70 | | ssexg 5230 |
. . . . . . . 8
⊢ ((𝑇 ⊆ (𝑇 ∪ {𝐽}) ∧ (𝑇 ∪ {𝐽}) ∈ V) → 𝑇 ∈ V) |
71 | 63, 69, 70 | sylancr 589 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑇 ∈ V) |
72 | 62, 71 | elmapd 8423 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑m 𝑇) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶𝑆)) |
73 | 59, 72 | mpbird 259 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑m 𝑇)) |
74 | | eleq1 2903 |
. . . . 5
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑m 𝑇))) |
75 | 73, 74 | syl5ibrcom 249 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → 𝑓 ∈ (𝑆 ↑m 𝑇))) |
76 | 75 | rexlimdvva 3297 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → 𝑓 ∈ (𝑆 ↑m 𝑇))) |
77 | 33, 76 | impbid 214 |
. 2
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}))) |
78 | | ralxpmap.j |
. . 3
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝜑 ↔ 𝜓)) |
79 | 78 | adantl 484 |
. 2
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) → (𝜑 ↔ 𝜓)) |
80 | 3, 77, 79 | ralxpxfr2d 3642 |
1
⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓)) |