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 32469 |
. 2
⊢
trCl(𝑋, 𝐴, 𝑅) = ∪
𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) |
6 | | ss2iun 4896 |
. . . 4
⊢
(∀𝑓 ∈
𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪
𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑓 ∈ 𝐵 𝐴) |
7 | | bnj1145.5 |
. . . . . . 7
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
8 | 7, 4 | bnj1083 32521 |
. . . . . 6
⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒) |
9 | 2 | bnj1095 32324 |
. . . . . . . . 9
⊢ (𝜓 → ∀𝑖𝜓) |
10 | 9, 7 | bnj1096 32325 |
. . . . . . . 8
⊢ (𝜒 → ∀𝑖𝜒) |
11 | 3 | bnj1098 32326 |
. . . . . . . . . . . . . . . . 17
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) |
12 | 7 | bnj1232 32346 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑛 ∈ 𝐷) |
13 | 12 | 3anim3i 1155 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) |
14 | 11, 13 | bnj1101 32327 |
. . . . . . . . . . . . . . . 16
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) |
15 | | ancl 548 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))) |
16 | 14, 15 | bnj101 32264 |
. . . . . . . . . . . . . . 15
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))) |
17 | | bnj1145.6 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))) |
18 | 17 | imbi2i 339 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))) |
19 | 18 | exbii 1854 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))) |
20 | 16, 19 | mpbir 234 |
. . . . . . . . . . . . . 14
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) |
21 | | bnj213 32425 |
. . . . . . . . . . . . . . . 16
⊢
pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
22 | 21 | bnj226 32275 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
23 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗) |
24 | 17, 23 | simplbiim 508 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜃 → 𝑖 = suc 𝑗) |
25 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛) |
26 | 12 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷) |
27 | 3 | bnj923 32310 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
28 | | elnn 7603 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω) |
29 | 27, 28 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω) |
30 | 25, 26, 29 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω) |
31 | 17, 30 | bnj832 32300 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜃 → 𝑖 ∈ ω) |
32 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑗 ∈ V |
33 | 32 | bnj216 32273 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖) |
34 | | elnn 7603 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω) |
35 | 33, 34 | sylan 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω) |
36 | 24, 31, 35 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → 𝑗 ∈ ω) |
37 | 17, 25 | bnj832 32300 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜃 → 𝑖 ∈ 𝑛) |
38 | 24, 37 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → suc 𝑗 ∈ 𝑛) |
39 | 2 | bnj589 32452 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
40 | 39 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
41 | 40 | bnj708 32298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
42 | | rsp 3117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑗 ∈
ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
44 | 7, 43 | sylbi 220 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
45 | 44 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
46 | 17, 45 | bnj832 32300 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))) |
47 | 36, 38, 46 | mp2d 49 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) |
48 | | fveqeq2 6677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = suc 𝑗 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
49 | 24, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))) |
50 | 47, 49 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (𝜃 → (𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) |
51 | 22, 50 | bnj1262 32353 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴) |
52 | 20, 51 | bnj1023 32323 |
. . . . . . . . . . . . 13
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
53 | | 3anass 1096 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒))) |
54 | 53 | imbi1i 353 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)) |
55 | 54 | exbii 1854 |
. . . . . . . . . . . . 13
⊢
(∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)) |
56 | 52, 55 | mpbi 233 |
. . . . . . . . . . . 12
⊢
∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴) |
57 | 1 | biimpi 219 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
58 | 7, 57 | bnj771 32306 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
59 | | fveq2 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅)) |
60 | | bnj213 32425 |
. . . . . . . . . . . . . . . 16
⊢
pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴 |
61 | | sseq1 3900 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴)) |
62 | 60, 61 | mpbiri 261 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴) |
63 | | sseq1 3900 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑖) = (𝑓‘∅) → ((𝑓‘𝑖) ⊆ 𝐴 ↔ (𝑓‘∅) ⊆ 𝐴)) |
64 | 63 | biimpar 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑖) = (𝑓‘∅) ∧ (𝑓‘∅) ⊆ 𝐴) → (𝑓‘𝑖) ⊆ 𝐴) |
65 | 59, 62, 64 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = ∅ ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) → (𝑓‘𝑖) ⊆ 𝐴) |
66 | 58, 65 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = ∅ ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
67 | 66 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((𝑖 = ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴) |
68 | 56, 67 | bnj1109 32329 |
. . . . . . . . . . 11
⊢
∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
69 | | 19.9v 1992 |
. . . . . . . . . . 11
⊢
(∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)) |
70 | 68, 69 | mpbi 233 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) |
71 | 70 | expcom 417 |
. . . . . . . . 9
⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)) |
72 | | fndm 6434 |
. . . . . . . . . . 11
⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛) |
73 | 7, 72 | bnj770 32305 |
. . . . . . . . . 10
⊢ (𝜒 → dom 𝑓 = 𝑛) |
74 | | eleq2 2821 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑛 → (𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛)) |
75 | 74 | imbi1d 345 |
. . . . . . . . . 10
⊢ (dom
𝑓 = 𝑛 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))) |
76 | 73, 75 | syl 17 |
. . . . . . . . 9
⊢ (𝜒 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))) |
77 | 71, 76 | mpbird 260 |
. . . . . . . 8
⊢ (𝜒 → (𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴)) |
78 | 10, 77 | hbralrimi 3094 |
. . . . . . 7
⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
79 | 78 | exlimiv 1936 |
. . . . . 6
⊢
(∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
80 | 8, 79 | sylbi 220 |
. . . . 5
⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
81 | | ss2iun 4896 |
. . . . . 6
⊢
(∀𝑖 ∈
dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑖 ∈ dom 𝑓 𝐴) |
82 | | bnj1143 32333 |
. . . . . 6
⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴 |
83 | 81, 82 | sstrdi 3887 |
. . . . 5
⊢
(∀𝑖 ∈
dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
84 | 80, 83 | syl 17 |
. . . 4
⊢ (𝑓 ∈ 𝐵 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴) |
85 | 6, 84 | mprg 3067 |
. . 3
⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑓 ∈ 𝐵 𝐴 |
86 | 4 | bnj1317 32364 |
. . . 4
⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵) |
87 | 86 | bnj1146 32334 |
. . 3
⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴 |
88 | 85, 87 | sstri 3884 |
. 2
⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 |
89 | 5, 88 | eqsstri 3909 |
1
⊢
trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴 |