Step | Hyp | Ref
| Expression |
1 | | bnj1145.1 |
. . 3
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
2 | | bnj1145.2 |
. . 3
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
3 | | bnj1145.3 |
. . 3
⊢ 𝐷 = (ω ∖
{∅}) |
4 | | bnj1145.4 |
. . 3
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
5 | 1, 2, 3, 4 | bnj882 30250 |
. 2
⊢
trCl(𝑋, 𝐴, 𝑅) = ∪
𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) |
6 | | ss2iun 4472 |
. . . 4
⊢
(∀𝑓 ∈
𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪
𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑓 ∈ 𝐵 𝐴) |
7 | | bnj1145.5 |
. . . . . . 7
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
8 | 7, 4 | bnj1083 30300 |
. . . . . 6
⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒) |
9 | 2 | bnj1095 30106 |
. . . . . . . . 9
⊢ (𝜓 → ∀𝑖𝜓) |
10 | 9, 7 | bnj1096 30107 |
. . . . . . . 8
⊢ (𝜒 → ∀𝑖𝜒) |
11 | 3 | bnj1098 30108 |
. . . . . . . . . . . . . . . . 17
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) |
12 | 7 | bnj1232 30128 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑛 ∈ 𝐷) |
13 | 12 | 3anim3i 1243 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) |
14 | 11, 13 | bnj1101 30109 |
. . . . . . . . . . . . . . . 16
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) |
15 | | ancl 567 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))) |
16 | 14, 15 | bnj101 30043 |
. . . . . . . . . . . . . . 15
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))) |
17 | | bnj1145.6 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))) |
18 | 17 | imbi2i 325 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))) |
19 | 18 | exbii 1764 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))) |
20 | 16, 19 | mpbir 220 |
. . . . . . . . . . . . . 14
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) |
21 | | bnj213 30206 |
. . . . . . . . . . . . . . . 16
⊢
pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
22 | 21 | bnj226 30056 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
23 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗) |
24 | 17, 23 | simplbiim 657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜃 → 𝑖 = suc 𝑗) |
25 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛) |
26 | 12 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷) |
27 | 3 | bnj923 30092 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
28 | | elnn 6967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω) |
29 | 27, 28 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω) |
30 | 25, 26, 29 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω) |
31 | 17, 30 | bnj832 30082 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜃 → 𝑖 ∈ ω) |
32 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑗 ∈ V |
33 | 32 | bnj216 30054 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖) |
34 | | elnn 6967 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω) |
35 | 33, 34 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω) |
36 | 24, 31, 35 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → 𝑗 ∈ ω) |
37 | 17, 25 | bnj832 30082 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜃 → 𝑖 ∈ 𝑛) |
38 | 24, 37 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → suc 𝑗 ∈ 𝑛) |
39 | 2 | bnj589 30233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
40 | 39 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
41 | 40 | bnj708 30080 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
42 | | rsp 2913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑗 ∈
ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
44 | 7, 43 | sylbi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
45 | 44 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
46 | 17, 45 | bnj832 30082 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
47 | 36, 38, 46 | mp2d 47 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) |
48 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = suc 𝑗 → (𝑓‘𝑖) = (𝑓‘suc 𝑗)) |
49 | 48 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = suc 𝑗 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
50 | 24, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
51 | 47, 50 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (𝜃 → (𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) |
52 | 22, 51 | bnj1262 30135 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴) |
53 | 20, 52 | bnj1023 30105 |
. . . . . . . . . . . . 13
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
54 | | 3anass 1035 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒))) |
55 | 54 | imbi1i 338 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)) |
56 | 55 | exbii 1764 |
. . . . . . . . . . . . 13
⊢
(∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)) |
57 | 53, 56 | mpbi 219 |
. . . . . . . . . . . 12
⊢
∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴) |
58 | 1 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
59 | 7, 58 | bnj771 30088 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅)) |
61 | | bnj213 30206 |
. . . . . . . . . . . . . . . 16
⊢
pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴 |
62 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴)) |
63 | 61, 62 | mpbiri 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴) |
64 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑖) = (𝑓‘∅) → ((𝑓‘𝑖) ⊆ 𝐴 ↔ (𝑓‘∅) ⊆ 𝐴)) |
65 | 64 | biimpar 501 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑖) = (𝑓‘∅) ∧ (𝑓‘∅) ⊆ 𝐴) → (𝑓‘𝑖) ⊆ 𝐴) |
66 | 60, 63, 65 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = ∅ ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) → (𝑓‘𝑖) ⊆ 𝐴) |
67 | 59, 66 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = ∅ ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
68 | 67 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝑖 = ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴) |
69 | 57, 68 | bnj1109 30111 |
. . . . . . . . . . 11
⊢
∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
70 | | 19.9v 1883 |
. . . . . . . . . . 11
⊢
(∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)) |
71 | 69, 70 | mpbi 219 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
72 | 71 | expcom 450 |
. . . . . . . . 9
⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)) |
73 | | fndm 5904 |
. . . . . . . . . . 11
⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛) |
74 | 7, 73 | bnj770 30087 |
. . . . . . . . . 10
⊢ (𝜒 → dom 𝑓 = 𝑛) |
75 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑛 → (𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛)) |
76 | 75 | imbi1d 330 |
. . . . . . . . . 10
⊢ (dom
𝑓 = 𝑛 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))) |
77 | 74, 76 | syl 17 |
. . . . . . . . 9
⊢ (𝜒 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))) |
78 | 72, 77 | mpbird 246 |
. . . . . . . 8
⊢ (𝜒 → (𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴)) |
79 | 10, 78 | hbralrimi 2937 |
. . . . . . 7
⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
80 | 79 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
81 | 8, 80 | sylbi 206 |
. . . . 5
⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
82 | | ss2iun 4472 |
. . . . . 6
⊢
(∀𝑖 ∈
dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑖 ∈ dom 𝑓 𝐴) |
83 | | bnj1143 30115 |
. . . . . 6
⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴 |
84 | 82, 83 | syl6ss 3580 |
. . . . 5
⊢
(∀𝑖 ∈
dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
85 | 81, 84 | syl 17 |
. . . 4
⊢ (𝑓 ∈ 𝐵 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
86 | 6, 85 | mprg 2910 |
. . 3
⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑓 ∈ 𝐵 𝐴 |
87 | 4 | bnj1317 30146 |
. . . 4
⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵) |
88 | 87 | bnj1146 30116 |
. . 3
⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴 |
89 | 86, 88 | sstri 3577 |
. 2
⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 |
90 | 5, 89 | eqsstri 3598 |
1
⊢
trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴 |