Proof of Theorem bnj1014
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bnj1014.14 | . . . . . . 7
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} | 
| 2 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑖𝐷 | 
| 3 |  | bnj1014.1 | . . . . . . . . . . 11
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) | 
| 4 |  | bnj1014.2 | . . . . . . . . . . 11
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 5 | 3, 4 | bnj911 34946 | . . . . . . . . . 10
⊢ ((𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑖(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | 
| 6 | 5 | nf5i 2146 | . . . . . . . . 9
⊢
Ⅎ𝑖(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) | 
| 7 | 2, 6 | nfrexw 3313 | . . . . . . . 8
⊢
Ⅎ𝑖∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) | 
| 8 | 7 | nfab 2911 | . . . . . . 7
⊢
Ⅎ𝑖{𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} | 
| 9 | 1, 8 | nfcxfr 2903 | . . . . . 6
⊢
Ⅎ𝑖𝐵 | 
| 10 | 9 | nfcri 2897 | . . . . 5
⊢
Ⅎ𝑖 𝑔 ∈ 𝐵 | 
| 11 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑖 𝑗 ∈ dom 𝑔 | 
| 12 | 10, 11 | nfan 1899 | . . . 4
⊢
Ⅎ𝑖(𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) | 
| 13 |  | nfv 1914 | . . . 4
⊢
Ⅎ𝑖(𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅) | 
| 14 | 12, 13 | nfim 1896 | . . 3
⊢
Ⅎ𝑖((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) | 
| 15 | 14 | nf5ri 2195 | . 2
⊢ (((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) → ∀𝑖((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅))) | 
| 16 |  | eleq1w 2824 | . . . . . 6
⊢ (𝑗 = 𝑖 → (𝑗 ∈ dom 𝑔 ↔ 𝑖 ∈ dom 𝑔)) | 
| 17 | 16 | anbi2d 630 | . . . . 5
⊢ (𝑗 = 𝑖 → ((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) ↔ (𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔))) | 
| 18 |  | fveq2 6906 | . . . . . 6
⊢ (𝑗 = 𝑖 → (𝑔‘𝑗) = (𝑔‘𝑖)) | 
| 19 | 18 | sseq1d 4015 | . . . . 5
⊢ (𝑗 = 𝑖 → ((𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅) ↔ (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅))) | 
| 20 | 17, 19 | imbi12d 344 | . . . 4
⊢ (𝑗 = 𝑖 → (((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) ↔ ((𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔) → (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)))) | 
| 21 | 20 | equcoms 2019 | . . 3
⊢ (𝑖 = 𝑗 → (((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) ↔ ((𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔) → (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)))) | 
| 22 | 1 | bnj1317 34835 | . . . . . . 7
⊢ (𝑔 ∈ 𝐵 → ∀𝑓 𝑔 ∈ 𝐵) | 
| 23 | 22 | nf5i 2146 | . . . . . 6
⊢
Ⅎ𝑓 𝑔 ∈ 𝐵 | 
| 24 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑓 𝑖 ∈ dom 𝑔 | 
| 25 | 23, 24 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑓(𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔) | 
| 26 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑓(𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅) | 
| 27 | 25, 26 | nfim 1896 | . . . 4
⊢
Ⅎ𝑓((𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔) → (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) | 
| 28 |  | eleq1w 2824 | . . . . . 6
⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝐵 ↔ 𝑔 ∈ 𝐵)) | 
| 29 |  | dmeq 5914 | . . . . . . 7
⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔) | 
| 30 | 29 | eleq2d 2827 | . . . . . 6
⊢ (𝑓 = 𝑔 → (𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ dom 𝑔)) | 
| 31 | 28, 30 | anbi12d 632 | . . . . 5
⊢ (𝑓 = 𝑔 → ((𝑓 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑓) ↔ (𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔))) | 
| 32 |  | fveq1 6905 | . . . . . 6
⊢ (𝑓 = 𝑔 → (𝑓‘𝑖) = (𝑔‘𝑖)) | 
| 33 | 32 | sseq1d 4015 | . . . . 5
⊢ (𝑓 = 𝑔 → ((𝑓‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅) ↔ (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅))) | 
| 34 | 31, 33 | imbi12d 344 | . . . 4
⊢ (𝑓 = 𝑔 → (((𝑓 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) ↔ ((𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔) → (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)))) | 
| 35 |  | ssiun2 5047 | . . . . 5
⊢ (𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖)) | 
| 36 |  | ssiun2 5047 | . . . . . 6
⊢ (𝑓 ∈ 𝐵 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪
𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)) | 
| 37 |  | bnj1014.13 | . . . . . . 7
⊢ 𝐷 = (ω ∖
{∅}) | 
| 38 | 3, 4, 37, 1 | bnj882 34940 | . . . . . 6
⊢ 
trCl(𝑋, 𝐴, 𝑅) = ∪
𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | 
| 39 | 36, 38 | sseqtrrdi 4025 | . . . . 5
⊢ (𝑓 ∈ 𝐵 → ∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) | 
| 40 | 35, 39 | sylan9ssr 3998 | . . . 4
⊢ ((𝑓 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) | 
| 41 | 27, 34, 40 | chvarfv 2240 | . . 3
⊢ ((𝑔 ∈ 𝐵 ∧ 𝑖 ∈ dom 𝑔) → (𝑔‘𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅)) | 
| 42 | 21, 41 | speivw 1973 | . 2
⊢
∃𝑖((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) | 
| 43 | 15, 42 | bnj1131 34801 | 1
⊢ ((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅)) |