Step | Hyp | Ref
| Expression |
1 | | eliun 4925 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 ↔ ∃𝑓 ∈ 𝐶 𝑧 ∈ dom 𝑓) |
2 | | bnj1498.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
3 | 2 | bnj1436 32719 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
4 | 3 | bnj1299 32698 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 𝑓 Fn 𝑑) |
5 | | fndm 6520 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Fn 𝑑 → dom 𝑓 = 𝑑) |
6 | 4, 5 | bnj31 32598 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
7 | 6 | bnj1196 32674 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → ∃𝑑(𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) |
8 | | bnj1498.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
9 | 8 | bnj1436 32719 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐵 → (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)) |
10 | 9 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ 𝐵 → 𝑑 ⊆ 𝐴) |
11 | 10 | anim1i 614 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑) → (𝑑 ⊆ 𝐴 ∧ dom 𝑓 = 𝑑)) |
12 | 7, 11 | bnj593 32625 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → ∃𝑑(𝑑 ⊆ 𝐴 ∧ dom 𝑓 = 𝑑)) |
13 | | sseq1 3942 |
. . . . . . . . . . . 12
⊢ (dom
𝑓 = 𝑑 → (dom 𝑓 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴)) |
14 | 13 | biimparc 479 |
. . . . . . . . . . 11
⊢ ((𝑑 ⊆ 𝐴 ∧ dom 𝑓 = 𝑑) → dom 𝑓 ⊆ 𝐴) |
15 | 12, 14 | bnj593 32625 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐶 → ∃𝑑dom 𝑓 ⊆ 𝐴) |
16 | 15 | bnj937 32651 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → dom 𝑓 ⊆ 𝐴) |
17 | 16 | sselda 3917 |
. . . . . . . 8
⊢ ((𝑓 ∈ 𝐶 ∧ 𝑧 ∈ dom 𝑓) → 𝑧 ∈ 𝐴) |
18 | 17 | rexlimiva 3209 |
. . . . . . 7
⊢
(∃𝑓 ∈
𝐶 𝑧 ∈ dom 𝑓 → 𝑧 ∈ 𝐴) |
19 | 1, 18 | sylbi 216 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 → 𝑧 ∈ 𝐴) |
20 | 2 | bnj1317 32701 |
. . . . . . 7
⊢ (𝑤 ∈ 𝐶 → ∀𝑓 𝑤 ∈ 𝐶) |
21 | 20 | bnj1400 32715 |
. . . . . 6
⊢ dom ∪ 𝐶 =
∪ 𝑓 ∈ 𝐶 dom 𝑓 |
22 | 19, 21 | eleq2s 2857 |
. . . . 5
⊢ (𝑧 ∈ dom ∪ 𝐶
→ 𝑧 ∈ 𝐴) |
23 | | bnj1498.4 |
. . . . . 6
⊢ 𝐹 = ∪
𝐶 |
24 | 23 | dmeqi 5802 |
. . . . 5
⊢ dom 𝐹 = dom ∪ 𝐶 |
25 | 22, 24 | eleq2s 2857 |
. . . 4
⊢ (𝑧 ∈ dom 𝐹 → 𝑧 ∈ 𝐴) |
26 | 25 | ssriv 3921 |
. . 3
⊢ dom 𝐹 ⊆ 𝐴 |
27 | 26 | a1i 11 |
. 2
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 ⊆ 𝐴) |
28 | | bnj1498.2 |
. . . . . . . 8
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
29 | 8, 28, 2 | bnj1493 32939 |
. . . . . . 7
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
30 | | vsnid 4595 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ {𝑥} |
31 | | elun1 4106 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → 𝑥 ∈ ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑥 ∈ ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) |
33 | | eleq2 2827 |
. . . . . . . . . 10
⊢ (dom
𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → (𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
34 | 32, 33 | mpbiri 257 |
. . . . . . . . 9
⊢ (dom
𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → 𝑥 ∈ dom 𝑓) |
35 | 34 | reximi 3174 |
. . . . . . . 8
⊢
(∃𝑓 ∈
𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
36 | 35 | ralimi 3086 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
37 | 29, 36 | syl 17 |
. . . . . 6
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
38 | | eliun 4925 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 ↔ ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
39 | 38 | ralbii 3090 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓 ↔ ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
40 | 37, 39 | sylibr 233 |
. . . . 5
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
41 | | nfcv 2906 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
42 | 8 | bnj1309 32902 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝐵 → ∀𝑥 𝑡 ∈ 𝐵) |
43 | 2, 42 | bnj1307 32903 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝐶 → ∀𝑥 𝑡 ∈ 𝐶) |
44 | 43 | nfcii 2890 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
45 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑥dom
𝑓 |
46 | 44, 45 | nfiun 4951 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑓 ∈ 𝐶 dom 𝑓 |
47 | 41, 46 | dfss3f 3908 |
. . . . 5
⊢ (𝐴 ⊆ ∪ 𝑓 ∈ 𝐶 dom 𝑓 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
48 | 40, 47 | sylibr 233 |
. . . 4
⊢ (𝑅 FrSe 𝐴 → 𝐴 ⊆ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
49 | 48, 21 | sseqtrrdi 3968 |
. . 3
⊢ (𝑅 FrSe 𝐴 → 𝐴 ⊆ dom ∪
𝐶) |
50 | 49, 24 | sseqtrrdi 3968 |
. 2
⊢ (𝑅 FrSe 𝐴 → 𝐴 ⊆ dom 𝐹) |
51 | 27, 50 | eqssd 3934 |
1
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴) |