Proof of Theorem frege131d
| Step | Hyp | Ref
| Expression |
| 1 | | frege131d.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
| 2 | | trclfvlb 15047 |
. . . . 5
⊢ (𝐹 ∈ V → 𝐹 ⊆ (t+‘𝐹)) |
| 3 | | imass1 6119 |
. . . . 5
⊢ (𝐹 ⊆ (t+‘𝐹) → (𝐹 “ 𝑈) ⊆ ((t+‘𝐹) “ 𝑈)) |
| 4 | 1, 2, 3 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝐹 “ 𝑈) ⊆ ((t+‘𝐹) “ 𝑈)) |
| 5 | | ssun2 4179 |
. . . . 5
⊢
((t+‘𝐹)
“ 𝑈) ⊆ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)) |
| 6 | | ssun2 4179 |
. . . . 5
⊢ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) |
| 7 | 5, 6 | sstri 3993 |
. . . 4
⊢
((t+‘𝐹)
“ 𝑈) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) |
| 8 | 4, 7 | sstrdi 3996 |
. . 3
⊢ (𝜑 → (𝐹 “ 𝑈) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 9 | | trclfvdecomr 43741 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ V → (t+‘𝐹) = (𝐹 ∪ ((t+‘𝐹) ∘ 𝐹))) |
| 10 | 1, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (t+‘𝐹) = (𝐹 ∪ ((t+‘𝐹) ∘ 𝐹))) |
| 11 | 10 | cnveqd 5886 |
. . . . . . . . . 10
⊢ (𝜑 → ◡(t+‘𝐹) = ◡(𝐹 ∪ ((t+‘𝐹) ∘ 𝐹))) |
| 12 | | cnvun 6162 |
. . . . . . . . . . 11
⊢ ◡(𝐹 ∪ ((t+‘𝐹) ∘ 𝐹)) = (◡𝐹 ∪ ◡((t+‘𝐹) ∘ 𝐹)) |
| 13 | | cnvco 5896 |
. . . . . . . . . . . 12
⊢ ◡((t+‘𝐹) ∘ 𝐹) = (◡𝐹 ∘ ◡(t+‘𝐹)) |
| 14 | 13 | uneq2i 4165 |
. . . . . . . . . . 11
⊢ (◡𝐹 ∪ ◡((t+‘𝐹) ∘ 𝐹)) = (◡𝐹 ∪ (◡𝐹 ∘ ◡(t+‘𝐹))) |
| 15 | 12, 14 | eqtri 2765 |
. . . . . . . . . 10
⊢ ◡(𝐹 ∪ ((t+‘𝐹) ∘ 𝐹)) = (◡𝐹 ∪ (◡𝐹 ∘ ◡(t+‘𝐹))) |
| 16 | 11, 15 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝜑 → ◡(t+‘𝐹) = (◡𝐹 ∪ (◡𝐹 ∘ ◡(t+‘𝐹)))) |
| 17 | 16 | coeq2d 5873 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ ◡(t+‘𝐹)) = (𝐹 ∘ (◡𝐹 ∪ (◡𝐹 ∘ ◡(t+‘𝐹))))) |
| 18 | | coundi 6267 |
. . . . . . . . 9
⊢ (𝐹 ∘ (◡𝐹 ∪ (◡𝐹 ∘ ◡(t+‘𝐹)))) = ((𝐹 ∘ ◡𝐹) ∪ (𝐹 ∘ (◡𝐹 ∘ ◡(t+‘𝐹)))) |
| 19 | | frege131d.fun |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
| 20 | | funcocnv2 6873 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹)) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹)) |
| 22 | | coass 6285 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∘ ◡𝐹) ∘ ◡(t+‘𝐹)) = (𝐹 ∘ (◡𝐹 ∘ ◡(t+‘𝐹))) |
| 23 | 22 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ (𝐹 ∘ (◡𝐹 ∘ ◡(t+‘𝐹))) = ((𝐹 ∘ ◡𝐹) ∘ ◡(t+‘𝐹)) |
| 24 | 21 | coeq1d 5872 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ∘ ◡𝐹) ∘ ◡(t+‘𝐹)) = (( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹))) |
| 25 | 23, 24 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ (◡𝐹 ∘ ◡(t+‘𝐹))) = (( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹))) |
| 26 | 21, 25 | uneq12d 4169 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ∘ ◡𝐹) ∪ (𝐹 ∘ (◡𝐹 ∘ ◡(t+‘𝐹)))) = (( I ↾ ran 𝐹) ∪ (( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)))) |
| 27 | 18, 26 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ (◡𝐹 ∪ (◡𝐹 ∘ ◡(t+‘𝐹)))) = (( I ↾ ran 𝐹) ∪ (( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)))) |
| 28 | 17, 27 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ ◡(t+‘𝐹)) = (( I ↾ ran 𝐹) ∪ (( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)))) |
| 29 | 28 | imaeq1d 6077 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) = ((( I ↾ ran 𝐹) ∪ (( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹))) “ 𝑈)) |
| 30 | | imaundir 6170 |
. . . . . 6
⊢ ((( I
↾ ran 𝐹) ∪ (( I
↾ ran 𝐹) ∘
◡(t+‘𝐹))) “ 𝑈) = ((( I ↾ ran 𝐹) “ 𝑈) ∪ ((( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)) “ 𝑈)) |
| 31 | 29, 30 | eqtrdi 2793 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) = ((( I ↾ ran 𝐹) “ 𝑈) ∪ ((( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)) “ 𝑈))) |
| 32 | | resss 6019 |
. . . . . . . . 9
⊢ ( I
↾ ran 𝐹) ⊆
I |
| 33 | | imass1 6119 |
. . . . . . . . 9
⊢ (( I
↾ ran 𝐹) ⊆ I
→ (( I ↾ ran 𝐹)
“ 𝑈) ⊆ ( I
“ 𝑈)) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
⊢ (( I
↾ ran 𝐹) “
𝑈) ⊆ ( I “
𝑈) |
| 35 | | imai 6092 |
. . . . . . . 8
⊢ ( I
“ 𝑈) = 𝑈 |
| 36 | 34, 35 | sseqtri 4032 |
. . . . . . 7
⊢ (( I
↾ ran 𝐹) “
𝑈) ⊆ 𝑈 |
| 37 | | imaco 6271 |
. . . . . . . 8
⊢ ((( I
↾ ran 𝐹) ∘
◡(t+‘𝐹)) “ 𝑈) = (( I ↾ ran 𝐹) “ (◡(t+‘𝐹) “ 𝑈)) |
| 38 | | imass1 6119 |
. . . . . . . . . 10
⊢ (( I
↾ ran 𝐹) ⊆ I
→ (( I ↾ ran 𝐹)
“ (◡(t+‘𝐹) “ 𝑈)) ⊆ ( I “ (◡(t+‘𝐹) “ 𝑈))) |
| 39 | 32, 38 | ax-mp 5 |
. . . . . . . . 9
⊢ (( I
↾ ran 𝐹) “
(◡(t+‘𝐹) “ 𝑈)) ⊆ ( I “ (◡(t+‘𝐹) “ 𝑈)) |
| 40 | | imai 6092 |
. . . . . . . . 9
⊢ ( I
“ (◡(t+‘𝐹) “ 𝑈)) = (◡(t+‘𝐹) “ 𝑈) |
| 41 | 39, 40 | sseqtri 4032 |
. . . . . . . 8
⊢ (( I
↾ ran 𝐹) “
(◡(t+‘𝐹) “ 𝑈)) ⊆ (◡(t+‘𝐹) “ 𝑈) |
| 42 | 37, 41 | eqsstri 4030 |
. . . . . . 7
⊢ ((( I
↾ ran 𝐹) ∘
◡(t+‘𝐹)) “ 𝑈) ⊆ (◡(t+‘𝐹) “ 𝑈) |
| 43 | | unss12 4188 |
. . . . . . 7
⊢ (((( I
↾ ran 𝐹) “
𝑈) ⊆ 𝑈 ∧ ((( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)) “ 𝑈) ⊆ (◡(t+‘𝐹) “ 𝑈)) → ((( I ↾ ran 𝐹) “ 𝑈) ∪ ((( I ↾ ran 𝐹) ∘ ◡(t+‘𝐹)) “ 𝑈)) ⊆ (𝑈 ∪ (◡(t+‘𝐹) “ 𝑈))) |
| 44 | 36, 42, 43 | mp2an 692 |
. . . . . 6
⊢ ((( I
↾ ran 𝐹) “
𝑈) ∪ ((( I ↾ ran
𝐹) ∘ ◡(t+‘𝐹)) “ 𝑈)) ⊆ (𝑈 ∪ (◡(t+‘𝐹) “ 𝑈)) |
| 45 | | ssun1 4178 |
. . . . . . 7
⊢ (𝑈 ∪ (◡(t+‘𝐹) “ 𝑈)) ⊆ ((𝑈 ∪ (◡(t+‘𝐹) “ 𝑈)) ∪ ((t+‘𝐹) “ 𝑈)) |
| 46 | | unass 4172 |
. . . . . . 7
⊢ ((𝑈 ∪ (◡(t+‘𝐹) “ 𝑈)) ∪ ((t+‘𝐹) “ 𝑈)) = (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) |
| 47 | 45, 46 | sseqtri 4032 |
. . . . . 6
⊢ (𝑈 ∪ (◡(t+‘𝐹) “ 𝑈)) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) |
| 48 | 44, 47 | sstri 3993 |
. . . . 5
⊢ ((( I
↾ ran 𝐹) “
𝑈) ∪ ((( I ↾ ran
𝐹) ∘ ◡(t+‘𝐹)) “ 𝑈)) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) |
| 49 | 31, 48 | eqsstrdi 4028 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 50 | | coss1 5866 |
. . . . . . . 8
⊢ (𝐹 ⊆ (t+‘𝐹) → (𝐹 ∘ (t+‘𝐹)) ⊆ ((t+‘𝐹) ∘ (t+‘𝐹))) |
| 51 | 1, 2, 50 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (t+‘𝐹)) ⊆ ((t+‘𝐹) ∘ (t+‘𝐹))) |
| 52 | | trclfvcotrg 15055 |
. . . . . . 7
⊢
((t+‘𝐹)
∘ (t+‘𝐹))
⊆ (t+‘𝐹) |
| 53 | 51, 52 | sstrdi 3996 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘ (t+‘𝐹)) ⊆ (t+‘𝐹)) |
| 54 | | imass1 6119 |
. . . . . 6
⊢ ((𝐹 ∘ (t+‘𝐹)) ⊆ (t+‘𝐹) → ((𝐹 ∘ (t+‘𝐹)) “ 𝑈) ⊆ ((t+‘𝐹) “ 𝑈)) |
| 55 | 53, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∘ (t+‘𝐹)) “ 𝑈) ⊆ ((t+‘𝐹) “ 𝑈)) |
| 56 | 55, 7 | sstrdi 3996 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘ (t+‘𝐹)) “ 𝑈) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 57 | 49, 56 | unssd 4192 |
. . 3
⊢ (𝜑 → (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈)) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 58 | 8, 57 | unssd 4192 |
. 2
⊢ (𝜑 → ((𝐹 “ 𝑈) ∪ (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈))) ⊆ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 59 | | frege131d.a |
. . . 4
⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 60 | 59 | imaeq2d 6078 |
. . 3
⊢ (𝜑 → (𝐹 “ 𝐴) = (𝐹 “ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))))) |
| 61 | | imaundi 6169 |
. . . 4
⊢ (𝐹 “ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) = ((𝐹 “ 𝑈) ∪ (𝐹 “ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) |
| 62 | | imaundi 6169 |
. . . . . 6
⊢ (𝐹 “ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) = ((𝐹 “ (◡(t+‘𝐹) “ 𝑈)) ∪ (𝐹 “ ((t+‘𝐹) “ 𝑈))) |
| 63 | | imaco 6271 |
. . . . . . . 8
⊢ ((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) = (𝐹 “ (◡(t+‘𝐹) “ 𝑈)) |
| 64 | 63 | eqcomi 2746 |
. . . . . . 7
⊢ (𝐹 “ (◡(t+‘𝐹) “ 𝑈)) = ((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) |
| 65 | | imaco 6271 |
. . . . . . . 8
⊢ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈) = (𝐹 “ ((t+‘𝐹) “ 𝑈)) |
| 66 | 65 | eqcomi 2746 |
. . . . . . 7
⊢ (𝐹 “ ((t+‘𝐹) “ 𝑈)) = ((𝐹 ∘ (t+‘𝐹)) “ 𝑈) |
| 67 | 64, 66 | uneq12i 4166 |
. . . . . 6
⊢ ((𝐹 “ (◡(t+‘𝐹) “ 𝑈)) ∪ (𝐹 “ ((t+‘𝐹) “ 𝑈))) = (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈)) |
| 68 | 62, 67 | eqtri 2765 |
. . . . 5
⊢ (𝐹 “ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))) = (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈)) |
| 69 | 68 | uneq2i 4165 |
. . . 4
⊢ ((𝐹 “ 𝑈) ∪ (𝐹 “ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) = ((𝐹 “ 𝑈) ∪ (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈))) |
| 70 | 61, 69 | eqtri 2765 |
. . 3
⊢ (𝐹 “ (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) = ((𝐹 “ 𝑈) ∪ (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈))) |
| 71 | 60, 70 | eqtrdi 2793 |
. 2
⊢ (𝜑 → (𝐹 “ 𝐴) = ((𝐹 “ 𝑈) ∪ (((𝐹 ∘ ◡(t+‘𝐹)) “ 𝑈) ∪ ((𝐹 ∘ (t+‘𝐹)) “ 𝑈)))) |
| 72 | 58, 71, 59 | 3sstr4d 4039 |
1
⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐴) |