| Step | Hyp | Ref
| Expression |
| 1 | | eliun 4995 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 ↔ ∃𝑓 ∈ 𝐶 𝑧 ∈ dom 𝑓) |
| 2 | | bnj1498.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
| 3 | 2 | bnj1436 34853 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
| 4 | 3 | bnj1299 34832 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 𝑓 Fn 𝑑) |
| 5 | | fndm 6671 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Fn 𝑑 → dom 𝑓 = 𝑑) |
| 6 | 4, 5 | bnj31 34733 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
| 7 | 6 | bnj1196 34808 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → ∃𝑑(𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) |
| 8 | | bnj1498.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
| 9 | 8 | bnj1436 34853 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐵 → (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)) |
| 10 | 9 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ 𝐵 → 𝑑 ⊆ 𝐴) |
| 11 | 10 | anim1i 615 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑) → (𝑑 ⊆ 𝐴 ∧ dom 𝑓 = 𝑑)) |
| 12 | 7, 11 | bnj593 34759 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → ∃𝑑(𝑑 ⊆ 𝐴 ∧ dom 𝑓 = 𝑑)) |
| 13 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (dom
𝑓 = 𝑑 → (dom 𝑓 ⊆ 𝐴 ↔ 𝑑 ⊆ 𝐴)) |
| 14 | 13 | biimparc 479 |
. . . . . . . . . . 11
⊢ ((𝑑 ⊆ 𝐴 ∧ dom 𝑓 = 𝑑) → dom 𝑓 ⊆ 𝐴) |
| 15 | 12, 14 | bnj593 34759 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐶 → ∃𝑑dom 𝑓 ⊆ 𝐴) |
| 16 | 15 | bnj937 34785 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → dom 𝑓 ⊆ 𝐴) |
| 17 | 16 | sselda 3983 |
. . . . . . . 8
⊢ ((𝑓 ∈ 𝐶 ∧ 𝑧 ∈ dom 𝑓) → 𝑧 ∈ 𝐴) |
| 18 | 17 | rexlimiva 3147 |
. . . . . . 7
⊢
(∃𝑓 ∈
𝐶 𝑧 ∈ dom 𝑓 → 𝑧 ∈ 𝐴) |
| 19 | 1, 18 | sylbi 217 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 → 𝑧 ∈ 𝐴) |
| 20 | 2 | bnj1317 34835 |
. . . . . . 7
⊢ (𝑤 ∈ 𝐶 → ∀𝑓 𝑤 ∈ 𝐶) |
| 21 | 20 | bnj1400 34849 |
. . . . . 6
⊢ dom ∪ 𝐶 =
∪ 𝑓 ∈ 𝐶 dom 𝑓 |
| 22 | 19, 21 | eleq2s 2859 |
. . . . 5
⊢ (𝑧 ∈ dom ∪ 𝐶
→ 𝑧 ∈ 𝐴) |
| 23 | | bnj1498.4 |
. . . . . 6
⊢ 𝐹 = ∪
𝐶 |
| 24 | 23 | dmeqi 5915 |
. . . . 5
⊢ dom 𝐹 = dom ∪ 𝐶 |
| 25 | 22, 24 | eleq2s 2859 |
. . . 4
⊢ (𝑧 ∈ dom 𝐹 → 𝑧 ∈ 𝐴) |
| 26 | 25 | ssriv 3987 |
. . 3
⊢ dom 𝐹 ⊆ 𝐴 |
| 27 | 26 | a1i 11 |
. 2
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 ⊆ 𝐴) |
| 28 | | bnj1498.2 |
. . . . . . . 8
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
| 29 | 8, 28, 2 | bnj1493 35073 |
. . . . . . 7
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
| 30 | | vsnid 4663 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ {𝑥} |
| 31 | | elun1 4182 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → 𝑥 ∈ ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
| 32 | 30, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑥 ∈ ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) |
| 33 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (dom
𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → (𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
| 34 | 32, 33 | mpbiri 258 |
. . . . . . . . 9
⊢ (dom
𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → 𝑥 ∈ dom 𝑓) |
| 35 | 34 | reximi 3084 |
. . . . . . . 8
⊢
(∃𝑓 ∈
𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
| 36 | 35 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
| 37 | 29, 36 | syl 17 |
. . . . . 6
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
| 38 | | eliun 4995 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 ↔ ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
| 39 | 38 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓 ↔ ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
| 40 | 37, 39 | sylibr 234 |
. . . . 5
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
| 41 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
| 42 | 8 | bnj1309 35036 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝐵 → ∀𝑥 𝑡 ∈ 𝐵) |
| 43 | 2, 42 | bnj1307 35037 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝐶 → ∀𝑥 𝑡 ∈ 𝐶) |
| 44 | 43 | nfcii 2894 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
| 45 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥dom
𝑓 |
| 46 | 44, 45 | nfiun 5023 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑓 ∈ 𝐶 dom 𝑓 |
| 47 | 41, 46 | dfss3f 3975 |
. . . . 5
⊢ (𝐴 ⊆ ∪ 𝑓 ∈ 𝐶 dom 𝑓 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
| 48 | 40, 47 | sylibr 234 |
. . . 4
⊢ (𝑅 FrSe 𝐴 → 𝐴 ⊆ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
| 49 | 48, 21 | sseqtrrdi 4025 |
. . 3
⊢ (𝑅 FrSe 𝐴 → 𝐴 ⊆ dom ∪
𝐶) |
| 50 | 49, 24 | sseqtrrdi 4025 |
. 2
⊢ (𝑅 FrSe 𝐴 → 𝐴 ⊆ dom 𝐹) |
| 51 | 27, 50 | eqssd 4001 |
1
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴) |