Proof of Theorem txindislem
| Step | Hyp | Ref
| Expression |
| 1 | | 0xp 5784 |
. . 3
⊢ (∅
× ( I ‘𝐵)) =
∅ |
| 2 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐴 ∈ V → ( I
‘𝐴) =
∅) |
| 3 | 2 | xpeq1d 5714 |
. . 3
⊢ (¬
𝐴 ∈ V → (( I
‘𝐴) × ( I
‘𝐵)) = (∅
× ( I ‘𝐵))) |
| 4 | | simpr 484 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 = ∅) → 𝐵 = ∅) |
| 5 | 4 | xpeq2d 5715 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 = ∅) → (𝐴 × 𝐵) = (𝐴 × ∅)) |
| 6 | | xp0 6178 |
. . . . . . 7
⊢ (𝐴 × ∅) =
∅ |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . . 6
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) |
| 8 | 7 | fveq2d 6910 |
. . . . 5
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 = ∅) → ( I
‘(𝐴 × 𝐵)) = ( I
‘∅)) |
| 9 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 10 | | fvi 6985 |
. . . . . 6
⊢ (∅
∈ V → ( I ‘∅) = ∅) |
| 11 | 9, 10 | ax-mp 5 |
. . . . 5
⊢ ( I
‘∅) = ∅ |
| 12 | 8, 11 | eqtrdi 2793 |
. . . 4
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 = ∅) → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 13 | | dmexg 7923 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ∈ V → dom (𝐴 × 𝐵) ∈ V) |
| 14 | | dmxp 5939 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
| 15 | 14 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝐵 ≠ ∅ → (dom (𝐴 × 𝐵) ∈ V ↔ 𝐴 ∈ V)) |
| 16 | 13, 15 | imbitrid 244 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ → ((𝐴 × 𝐵) ∈ V → 𝐴 ∈ V)) |
| 17 | 16 | con3d 152 |
. . . . . 6
⊢ (𝐵 ≠ ∅ → (¬
𝐴 ∈ V → ¬
(𝐴 × 𝐵) ∈ V)) |
| 18 | 17 | impcom 407 |
. . . . 5
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ≠ ∅) → ¬
(𝐴 × 𝐵) ∈ V) |
| 19 | | fvprc 6898 |
. . . . 5
⊢ (¬
(𝐴 × 𝐵) ∈ V → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 20 | 18, 19 | syl 17 |
. . . 4
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ≠ ∅) → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 21 | 12, 20 | pm2.61dane 3029 |
. . 3
⊢ (¬
𝐴 ∈ V → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 22 | 1, 3, 21 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝐴 ∈ V → (( I
‘𝐴) × ( I
‘𝐵)) = ( I
‘(𝐴 × 𝐵))) |
| 23 | | xp0 6178 |
. . 3
⊢ (( I
‘𝐴) × ∅)
= ∅ |
| 24 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐵 ∈ V → ( I
‘𝐵) =
∅) |
| 25 | 24 | xpeq2d 5715 |
. . 3
⊢ (¬
𝐵 ∈ V → (( I
‘𝐴) × ( I
‘𝐵)) = (( I
‘𝐴) ×
∅)) |
| 26 | | simpr 484 |
. . . . . . . 8
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 = ∅) → 𝐴 = ∅) |
| 27 | 26 | xpeq1d 5714 |
. . . . . . 7
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 = ∅) → (𝐴 × 𝐵) = (∅ × 𝐵)) |
| 28 | | 0xp 5784 |
. . . . . . 7
⊢ (∅
× 𝐵) =
∅ |
| 29 | 27, 28 | eqtrdi 2793 |
. . . . . 6
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 = ∅) → (𝐴 × 𝐵) = ∅) |
| 30 | 29 | fveq2d 6910 |
. . . . 5
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 = ∅) → ( I
‘(𝐴 × 𝐵)) = ( I
‘∅)) |
| 31 | 30, 11 | eqtrdi 2793 |
. . . 4
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 = ∅) → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 32 | | rnexg 7924 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ∈ V → ran (𝐴 × 𝐵) ∈ V) |
| 33 | | rnxp 6190 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
| 34 | 33 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ → (ran (𝐴 × 𝐵) ∈ V ↔ 𝐵 ∈ V)) |
| 35 | 32, 34 | imbitrid 244 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ V → 𝐵 ∈ V)) |
| 36 | 35 | con3d 152 |
. . . . . 6
⊢ (𝐴 ≠ ∅ → (¬
𝐵 ∈ V → ¬
(𝐴 × 𝐵) ∈ V)) |
| 37 | 36 | impcom 407 |
. . . . 5
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 ≠ ∅) → ¬
(𝐴 × 𝐵) ∈ V) |
| 38 | 37, 19 | syl 17 |
. . . 4
⊢ ((¬
𝐵 ∈ V ∧ 𝐴 ≠ ∅) → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 39 | 31, 38 | pm2.61dane 3029 |
. . 3
⊢ (¬
𝐵 ∈ V → ( I
‘(𝐴 × 𝐵)) = ∅) |
| 40 | 23, 25, 39 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝐵 ∈ V → (( I
‘𝐴) × ( I
‘𝐵)) = ( I
‘(𝐴 × 𝐵))) |
| 41 | | fvi 6985 |
. . . 4
⊢ (𝐴 ∈ V → ( I
‘𝐴) = 𝐴) |
| 42 | | fvi 6985 |
. . . 4
⊢ (𝐵 ∈ V → ( I
‘𝐵) = 𝐵) |
| 43 | | xpeq12 5710 |
. . . 4
⊢ ((( I
‘𝐴) = 𝐴 ∧ ( I ‘𝐵) = 𝐵) → (( I ‘𝐴) × ( I ‘𝐵)) = (𝐴 × 𝐵)) |
| 44 | 41, 42, 43 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (( I
‘𝐴) × ( I
‘𝐵)) = (𝐴 × 𝐵)) |
| 45 | | xpexg 7770 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V) |
| 46 | | fvi 6985 |
. . . 4
⊢ ((𝐴 × 𝐵) ∈ V → ( I ‘(𝐴 × 𝐵)) = (𝐴 × 𝐵)) |
| 47 | 45, 46 | syl 17 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ( I
‘(𝐴 × 𝐵)) = (𝐴 × 𝐵)) |
| 48 | 44, 47 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (( I
‘𝐴) × ( I
‘𝐵)) = ( I
‘(𝐴 × 𝐵))) |
| 49 | 22, 40, 48 | ecase 1034 |
1
⊢ (( I
‘𝐴) × ( I
‘𝐵)) = ( I
‘(𝐴 × 𝐵)) |