Step | Hyp | Ref
| Expression |
1 | | vex 3477 |
. . 3
⊢ 𝑔 ∈ V |
2 | | snex 5431 |
. . 3
⊢
{⟨𝐽, 𝑦⟩} ∈
V |
3 | 1, 2 | unex 7737 |
. 2
⊢ (𝑔 ∪ {⟨𝐽, 𝑦⟩}) ∈ V |
4 | | simpr 484 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 ∈ (𝑆 ↑m 𝑇)) |
5 | | elmapex 8846 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑆 ↑m 𝑇) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
7 | | elmapg 8837 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ 𝑓:𝑇⟶𝑆)) |
9 | 4, 8 | mpbid 231 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓:𝑇⟶𝑆) |
10 | | simpl 482 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝐽 ∈ 𝑇) |
11 | 9, 10 | ffvelcdmd 7087 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓‘𝐽) ∈ 𝑆) |
12 | | difss 4131 |
. . . . . . 7
⊢ (𝑇 ∖ {𝐽}) ⊆ 𝑇 |
13 | | fssres 6757 |
. . . . . . 7
⊢ ((𝑓:𝑇⟶𝑆 ∧ (𝑇 ∖ {𝐽}) ⊆ 𝑇) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
14 | 9, 12, 13 | sylancl 585 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆) |
15 | 5 | simpld 494 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑆 ↑m 𝑇) → 𝑆 ∈ V) |
16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑆 ∈ V) |
17 | 6 | simprd 495 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑇 ∈ V) |
18 | 17 | difexd 5329 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑇 ∖ {𝐽}) ∈ V) |
19 | 16, 18 | elmapd 8838 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) ↔ (𝑓 ↾ (𝑇 ∖ {𝐽})):(𝑇 ∖ {𝐽})⟶𝑆)) |
20 | 14, 19 | mpbird 257 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))) |
21 | 9 | ffnd 6718 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 Fn 𝑇) |
22 | | fnsnsplit 7184 |
. . . . . 6
⊢ ((𝑓 Fn 𝑇 ∧ 𝐽 ∈ 𝑇) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {⟨𝐽, (𝑓‘𝐽)⟩})) |
23 | 21, 10, 22 | syl2anc 583 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {⟨𝐽, (𝑓‘𝐽)⟩})) |
24 | | opeq2 4874 |
. . . . . . . . 9
⊢ (𝑦 = (𝑓‘𝐽) → ⟨𝐽, 𝑦⟩ = ⟨𝐽, (𝑓‘𝐽)⟩) |
25 | 24 | sneqd 4640 |
. . . . . . . 8
⊢ (𝑦 = (𝑓‘𝐽) → {⟨𝐽, 𝑦⟩} = {⟨𝐽, (𝑓‘𝐽)⟩}) |
26 | 25 | uneq2d 4163 |
. . . . . . 7
⊢ (𝑦 = (𝑓‘𝐽) → (𝑔 ∪ {⟨𝐽, 𝑦⟩}) = (𝑔 ∪ {⟨𝐽, (𝑓‘𝐽)⟩})) |
27 | 26 | eqeq2d 2742 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝐽) → (𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) ↔ 𝑓 = (𝑔 ∪ {⟨𝐽, (𝑓‘𝐽)⟩}))) |
28 | | uneq1 4156 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑔 ∪ {⟨𝐽, (𝑓‘𝐽)⟩}) = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {⟨𝐽, (𝑓‘𝐽)⟩})) |
29 | 28 | eqeq2d 2742 |
. . . . . 6
⊢ (𝑔 = (𝑓 ↾ (𝑇 ∖ {𝐽})) → (𝑓 = (𝑔 ∪ {⟨𝐽, (𝑓‘𝐽)⟩}) ↔ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {⟨𝐽, (𝑓‘𝐽)⟩}))) |
30 | 27, 29 | rspc2ev 3624 |
. . . . 5
⊢ (((𝑓‘𝐽) ∈ 𝑆 ∧ (𝑓 ↾ (𝑇 ∖ {𝐽})) ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) ∧ 𝑓 = ((𝑓 ↾ (𝑇 ∖ {𝐽})) ∪ {⟨𝐽, (𝑓‘𝐽)⟩})) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩})) |
31 | 11, 20, 23, 30 | syl3anc 1370 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 ∈ (𝑆 ↑m 𝑇)) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩})) |
32 | 31 | ex 412 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑m 𝑇) → ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}))) |
33 | | elmapi 8847 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
34 | 33 | ad2antll 726 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑔:(𝑇 ∖ {𝐽})⟶𝑆) |
35 | | f1osng 6874 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {⟨𝐽, 𝑦⟩}:{𝐽}–1-1-onto→{𝑦}) |
36 | | f1of 6833 |
. . . . . . . . . . . 12
⊢
({⟨𝐽, 𝑦⟩}:{𝐽}–1-1-onto→{𝑦} → {⟨𝐽, 𝑦⟩}:{𝐽}⟶{𝑦}) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V) → {⟨𝐽, 𝑦⟩}:{𝐽}⟶{𝑦}) |
38 | 37 | elvd 3480 |
. . . . . . . . . 10
⊢ (𝐽 ∈ 𝑇 → {⟨𝐽, 𝑦⟩}:{𝐽}⟶{𝑦}) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {⟨𝐽, 𝑦⟩}:{𝐽}⟶{𝑦}) |
40 | | disjdifr 4472 |
. . . . . . . . . 10
⊢ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅ |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) |
42 | | fun 6753 |
. . . . . . . . 9
⊢ (((𝑔:(𝑇 ∖ {𝐽})⟶𝑆 ∧ {⟨𝐽, 𝑦⟩}:{𝐽}⟶{𝑦}) ∧ ((𝑇 ∖ {𝐽}) ∩ {𝐽}) = ∅) → (𝑔 ∪ {⟨𝐽, 𝑦⟩}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
43 | 34, 39, 41, 42 | syl21anc 835 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {⟨𝐽, 𝑦⟩}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦})) |
44 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝐽 ∈ 𝑇) |
45 | 44 | snssd 4812 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {𝐽} ⊆ 𝑇) |
46 | | undifr 4482 |
. . . . . . . . . 10
⊢ ({𝐽} ⊆ 𝑇 ↔ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = 𝑇) |
47 | 45, 46 | sylib 217 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = 𝑇) |
48 | 47 | feq2d 6703 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {⟨𝐽, 𝑦⟩}):((𝑇 ∖ {𝐽}) ∪ {𝐽})⟶(𝑆 ∪ {𝑦}) ↔ (𝑔 ∪ {⟨𝐽, 𝑦⟩}):𝑇⟶(𝑆 ∪ {𝑦}))) |
49 | 43, 48 | mpbid 231 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {⟨𝐽, 𝑦⟩}):𝑇⟶(𝑆 ∪ {𝑦})) |
50 | | ssidd 4005 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑆 ⊆ 𝑆) |
51 | | snssi 4811 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 → {𝑦} ⊆ 𝑆) |
52 | 51 | ad2antrl 725 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → {𝑦} ⊆ 𝑆) |
53 | 50, 52 | unssd 4186 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑆 ∪ {𝑦}) ⊆ 𝑆) |
54 | 49, 53 | fssd 6735 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {⟨𝐽, 𝑦⟩}):𝑇⟶𝑆) |
55 | | elmapex 8846 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
56 | 55 | ad2antll 726 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑆 ∈ V ∧ (𝑇 ∖ {𝐽}) ∈ V)) |
57 | 56 | simpld 494 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑆 ∈ V) |
58 | | ssun1 4172 |
. . . . . . . 8
⊢ 𝑇 ⊆ (𝑇 ∪ {𝐽}) |
59 | | undif1 4475 |
. . . . . . . . 9
⊢ ((𝑇 ∖ {𝐽}) ∪ {𝐽}) = (𝑇 ∪ {𝐽}) |
60 | 56 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑇 ∖ {𝐽}) ∈ V) |
61 | | snex 5431 |
. . . . . . . . . 10
⊢ {𝐽} ∈ V |
62 | | unexg 7740 |
. . . . . . . . . 10
⊢ (((𝑇 ∖ {𝐽}) ∈ V ∧ {𝐽} ∈ V) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
63 | 60, 61, 62 | sylancl 585 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑇 ∖ {𝐽}) ∪ {𝐽}) ∈ V) |
64 | 59, 63 | eqeltrrid 2837 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑇 ∪ {𝐽}) ∈ V) |
65 | | ssexg 5323 |
. . . . . . . 8
⊢ ((𝑇 ⊆ (𝑇 ∪ {𝐽}) ∧ (𝑇 ∪ {𝐽}) ∈ V) → 𝑇 ∈ V) |
66 | 58, 64, 65 | sylancr 586 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → 𝑇 ∈ V) |
67 | 57, 66 | elmapd 8838 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → ((𝑔 ∪ {⟨𝐽, 𝑦⟩}) ∈ (𝑆 ↑m 𝑇) ↔ (𝑔 ∪ {⟨𝐽, 𝑦⟩}):𝑇⟶𝑆)) |
68 | 54, 67 | mpbird 257 |
. . . . 5
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑔 ∪ {⟨𝐽, 𝑦⟩}) ∈ (𝑆 ↑m 𝑇)) |
69 | | eleq1 2820 |
. . . . 5
⊢ (𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ (𝑔 ∪ {⟨𝐽, 𝑦⟩}) ∈ (𝑆 ↑m 𝑇))) |
70 | 68, 69 | syl5ibrcom 246 |
. . . 4
⊢ ((𝐽 ∈ 𝑇 ∧ (𝑦 ∈ 𝑆 ∧ 𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽})))) → (𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) → 𝑓 ∈ (𝑆 ↑m 𝑇))) |
71 | 70 | rexlimdvva 3210 |
. . 3
⊢ (𝐽 ∈ 𝑇 → (∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) → 𝑓 ∈ (𝑆 ↑m 𝑇))) |
72 | 32, 71 | impbid 211 |
. 2
⊢ (𝐽 ∈ 𝑇 → (𝑓 ∈ (𝑆 ↑m 𝑇) ↔ ∃𝑦 ∈ 𝑆 ∃𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}))) |
73 | | ralxpmap.j |
. . 3
⊢ (𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) → (𝜑 ↔ 𝜓)) |
74 | 73 | adantl 481 |
. 2
⊢ ((𝐽 ∈ 𝑇 ∧ 𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩})) → (𝜑 ↔ 𝜓)) |
75 | 3, 72, 74 | ralxpxfr2d 3634 |
1
⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓)) |