| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ltbval.c | . 2
⊢ 𝐶 = (𝑇 <bag 𝐼) | 
| 2 |  | ltbval.t | . . 3
⊢ (𝜑 → 𝑇 ∈ 𝑊) | 
| 3 |  | ltbval.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 4 |  | elex 3500 | . . . 4
⊢ (𝑇 ∈ 𝑊 → 𝑇 ∈ V) | 
| 5 |  | elex 3500 | . . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ V) | 
| 6 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼) | 
| 7 | 6 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → (ℕ0
↑m 𝑖) =
(ℕ0 ↑m 𝐼)) | 
| 8 |  | rabeq 3450 | . . . . . . . . . 10
⊢
((ℕ0 ↑m 𝑖) = (ℕ0 ↑m
𝐼) → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . 9
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 10 |  | ltbval.d | . . . . . . . . 9
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 11 | 9, 10 | eqtr4di 2794 | . . . . . . . 8
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷) | 
| 12 | 11 | sseq2d 4015 | . . . . . . 7
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ↔ {𝑥, 𝑦} ⊆ 𝐷)) | 
| 13 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → 𝑟 = 𝑇) | 
| 14 | 13 | breqd 5153 | . . . . . . . . . . 11
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → (𝑧𝑟𝑤 ↔ 𝑧𝑇𝑤)) | 
| 15 | 14 | imbi1d 341 | . . . . . . . . . 10
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → ((𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 16 | 6, 15 | raleqbidv 3345 | . . . . . . . . 9
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → (∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) | 
| 17 | 16 | anbi2d 630 | . . . . . . . 8
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → (((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) | 
| 18 | 6, 17 | rexeqbidv 3346 | . . . . . . 7
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → (∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) | 
| 19 | 12, 18 | anbi12d 632 | . . . . . 6
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → (({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧
∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) ↔ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))) | 
| 20 | 19 | opabbidv 5208 | . . . . 5
⊢ ((𝑟 = 𝑇 ∧ 𝑖 = 𝐼) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧
∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | 
| 21 |  | df-ltbag 21933 | . . . . 5
⊢ 
<bag = (𝑟
∈ V, 𝑖 ∈ V
↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧
∃𝑧 ∈ 𝑖 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑖 (𝑧𝑟𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | 
| 22 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 23 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑦 ∈ V | 
| 24 | 22, 23 | prss 4819 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ {𝑥, 𝑦} ⊆ 𝐷) | 
| 25 | 24 | anbi1i 624 | . . . . . . 7
⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) ↔ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) | 
| 26 | 25 | opabbii 5209 | . . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))} | 
| 27 |  | ovex 7465 | . . . . . . . . 9
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 28 | 10, 27 | rabex2 5340 | . . . . . . . 8
⊢ 𝐷 ∈ V | 
| 29 | 28, 28 | xpex 7774 | . . . . . . 7
⊢ (𝐷 × 𝐷) ∈ V | 
| 30 |  | opabssxp 5777 | . . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))} ⊆ (𝐷 × 𝐷) | 
| 31 | 29, 30 | ssexi 5321 | . . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))} ∈ V | 
| 32 | 26, 31 | eqeltrri 2837 | . . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))} ∈ V | 
| 33 | 20, 21, 32 | ovmpoa 7589 | . . . 4
⊢ ((𝑇 ∈ V ∧ 𝐼 ∈ V) → (𝑇 <bag 𝐼) = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | 
| 34 | 4, 5, 33 | syl2an 596 | . . 3
⊢ ((𝑇 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉) → (𝑇 <bag 𝐼) = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | 
| 35 | 2, 3, 34 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑇 <bag 𝐼) = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) | 
| 36 | 1, 35 | eqtrid 2788 | 1
⊢ (𝜑 → 𝐶 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ∃𝑧 ∈ 𝐼 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐼 (𝑧𝑇𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))}) |