Proof of Theorem ralxpmap
Step | Hyp | Ref
| Expression |
1 | | vex 3412 |
. . 3
⊢ 𝑔 ∈ V |
2 | | snex 5324 |
. . 3
⊢
{〈𝐽, 𝑦〉} ∈
V |
3 | 1, 2 | unex 7531 |
. 2
⊢ (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ V |
4 | | simpr 488 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 ∈ (𝑆 ↑m 𝑇)) |
5 | | elmapex 8529 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑆 ↑m 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
6 | 5 | adantl 485 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
7 | | elmapg 8521 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
9 | 4, 8 | mpbid 235 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓:𝑇⟶𝑆) |
10 | | simpl 486 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝐽 ∈ 𝑇) |
11 | 9, 10 | ffvelrnd 6905 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓‘𝐽) ∈ 𝑆) |
12 | | difss 4046 |
. . . . . . 7
⊢ (𝑇 ∖ {𝐽}) ⊆ 𝑇 |
13 | | fssres 6585 |
. . . . . . 7
⊢ ((𝑓:𝑇⟶𝑆 ∧ (𝑇 ∖ {𝐽}) ⊆ 𝑇) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
14 | 9, 12, 13 | sylancl 589 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
15 | 5 | simpld 498 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑆 ↑m 𝑇) → 𝑆 ∈ V) |
16 | 15 | adantl 485 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑆 ∈ V) |
17 | 6 | simprd 499 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑇 ∈ V) |
18 | 17 | difexd 5222 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑇 ∖ {𝐽}) ∈ V) |
19 | 16, 18 | elmapd 8522 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) ↔ (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆)) |
20 | 14, 19 | mpbird 260 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))) |
21 | 9 | ffnd 6546 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 Fn 𝑇) |
22 | | fnsnsplit 6999 |
. . . . . 6
⊢ ((𝑓 Fn 𝑇 ∧ 𝐽 ∈ 𝑇) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
23 | 21, 10, 22 | syl2anc 587 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
24 | | opeq2 4785 |
. . . . . . . . 9
⊢ (𝑦 = (𝑓‘𝐽) → 〈𝐽, 𝑦〉 = 〈𝐽, (𝑓‘𝐽)〉) |
25 | 24 | sneqd 4553 |
. . . . . . . 8
⊢ (𝑦 = (𝑓‘𝐽) → {〈𝐽, 𝑦〉} = {〈𝐽, (𝑓‘𝐽)〉}) |
26 | 25 | uneq2d 4077 |
. . . . . . 7
⊢ (𝑦 = (𝑓‘𝐽) → (𝑔 ∪ {〈𝐽, 𝑦〉}) = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
27 | 26 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝐽) → (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) ↔ 𝑓 = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}))) |
28 | | uneq1 4070 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}) = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) |
29 | 28 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑓 = (𝑔 ∪ {〈𝐽, (𝑓‘𝐽)〉}) ↔ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉}))) |
30 | 27, 29 | rspc2ev 3549 |
. . . . 5
⊢ (((𝑓‘𝐽) ∈ 𝑆 ∧ (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) ∧ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {〈𝐽, (𝑓‘𝐽)〉})) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) |
31 | 11, 20, 23, 30 | syl3anc 1373 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) |
32 | 31 | ex 416 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑m 𝑇) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}))) |
33 | | elmapi 8530 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
34 | 33 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
35 | | f1osng 6701 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {〈𝐽, 𝑦〉}:{𝐽}–1-1-onto→{𝑦}) |
36 | | f1of 6661 |
. . . . . . . . . . . 12
⊢
({〈𝐽, 𝑦〉}:{𝐽}–1-1-onto→{𝑦} → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
38 | 37 | elvd 3415 |
. . . . . . . . . 10
⊢ (𝐽 ∈ 𝑇 → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
39 | 38 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) |
40 | | disjdifr 4387 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅ |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) |
42 | | fun 6581 |
. . . . . . . . 9
⊢ (((𝑔:(𝑇 ∖ {𝐽})⟶𝑆 ∧ {〈𝐽, 𝑦〉}:{𝐽}⟶{𝑦}) ∧ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) → (𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
43 | 34, 39, 41, 42 | syl21anc 838 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
44 | | uncom 4067 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = ({𝐽} ∪ (𝑇 ∖ {𝐽})) |
45 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝐽 ∈ 𝑇) |
46 | 45 | snssd 4722 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {𝐽} ⊆ 𝑇) |
47 | | undif 4396 |
. . . . . . . . . . 11
⊢ ({𝐽} ⊆ 𝑇 ↔ ({𝐽} ∪ (𝑇 ∖ {𝐽})) = 𝑇) |
48 | 46, 47 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ({𝐽} ∪ (𝑇 ∖ {𝐽})) = 𝑇) |
49 | 44, 48 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = 𝑇) |
50 | 49 | feq2d 6531 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {〈𝐽, 𝑦〉}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦}) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶(𝑆 ∪ {𝑦}))) |
51 | 43, 50 | mpbid 235 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶(𝑆 ∪ {𝑦})) |
52 | | ssidd 3924 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑆 ⊆ 𝑆) |
53 | | snssi 4721 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 → {𝑦} ⊆ 𝑆) |
54 | 53 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {𝑦} ⊆ 𝑆) |
55 | 52, 54 | unssd 4100 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑆 ∪ {𝑦}) ⊆ 𝑆) |
56 | 51, 55 | fssd 6563 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶𝑆) |
57 | | elmapex 8529 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
58 | 57 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
59 | 58 | simpld 498 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑆 ∈ V) |
60 | | ssun1 4086 |
. . . . . . . 8
⊢ 𝑇 ⊆ (𝑇 ∪ {𝐽}) |
61 | | undif1 4390 |
. . . . . . . . 9
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = (𝑇 ∪ {𝐽}) |
62 | 58 | simprd 499 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑇 ∖ {𝐽}) ∈ V) |
63 | | snex 5324 |
. . . . . . . . . 10
⊢ {𝐽} ∈ V |
64 | | unexg 7534 |
. . . . . . . . . 10
⊢ (((𝑇 ∖ {𝐽}) ∈ V ∧ {𝐽} ∈ V) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
65 | 62, 63, 64 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
66 | 61, 65 | eqeltrrid 2843 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑇 ∪ {𝐽}) ∈ V) |
67 | | ssexg 5216 |
. . . . . . . 8
⊢ ((𝑇 ⊆ (𝑇 ∪ {𝐽}) ∧ (𝑇 ∪ {𝐽}) ∈ V) → 𝑇 ∈ V) |
68 | 60, 66, 67 | sylancr 590 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑇 ∈ V) |
69 | 59, 68 | elmapd 8522 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑m 𝑇) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}):𝑇⟶𝑆)) |
70 | 56, 69 | mpbird 260 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑m 𝑇)) |
71 | | eleq1 2825 |
. . . . 5
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ (𝑔 ∪ {〈𝐽, 𝑦〉}) ∈ (𝑆 ↑m 𝑇))) |
72 | 70, 71 | syl5ibrcom 250 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → 𝑓 ∈ (𝑆 ↑m 𝑇))) |
73 | 72 | rexlimdvva 3213 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → 𝑓 ∈ (𝑆 ↑m 𝑇))) |
74 | 32, 73 | impbid 215 |
. 2
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}))) |
75 | | ralxpmap.j |
. . 3
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝜑 ↔ 𝜓)) |
76 | 75 | adantl 485 |
. 2
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉})) → (𝜑 ↔ 𝜓)) |
77 | 3, 74, 76 | ralxpxfr2d 3553 |
1
⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓)) |