| Step | Hyp | Ref
| Expression |
| 1 | | reldom 8991 |
. . . . 5
⊢ Rel
≼ |
| 2 | 1 | brrelex1i 5741 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
| 3 | 1 | brrelex1i 5741 |
. . . 4
⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V) |
| 4 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤)) |
| 5 | | breq2 5147 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴)) |
| 6 | 4, 5 | 3anbi23d 1441 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((𝑤 ∈ Fin ∧ 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) ↔ (𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴))) |
| 7 | | breq1 5146 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤)) |
| 8 | 6, 7 | imbi12d 344 |
. . . . 5
⊢ (𝑧 = 𝐴 → (((𝑤 ∈ Fin ∧ 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) ↔ ((𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤))) |
| 9 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝑤 ∈ Fin ↔ 𝐵 ∈ Fin)) |
| 10 | | breq2 5147 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵)) |
| 11 | | breq1 5146 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴)) |
| 12 | 9, 10, 11 | 3anbi123d 1438 |
. . . . . 6
⊢ (𝑤 = 𝐵 → ((𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) ↔ (𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
| 13 | | breq2 5147 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵)) |
| 14 | 12, 13 | imbi12d 344 |
. . . . 5
⊢ (𝑤 = 𝐵 → (((𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴) → 𝐴 ≈ 𝑤) ↔ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵))) |
| 15 | | vex 3484 |
. . . . . 6
⊢ 𝑧 ∈ V |
| 16 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧)) |
| 17 | | imaeq2 6074 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑓 “ 𝑦) = (𝑓 “ 𝑥)) |
| 18 | 17 | difeq2d 4126 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑤 ∖ (𝑓 “ 𝑦)) = (𝑤 ∖ (𝑓 “ 𝑥))) |
| 19 | 18 | imaeq2d 6078 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) = (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥)))) |
| 20 | | difeq2 4120 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑧 ∖ 𝑦) = (𝑧 ∖ 𝑥)) |
| 21 | 19, 20 | sseq12d 4017 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦) ↔ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))) |
| 22 | 16, 21 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦)) ↔ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥)))) |
| 23 | 22 | cbvabv 2812 |
. . . . . 6
⊢ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))} = {𝑥 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑥))) ⊆ (𝑧 ∖ 𝑥))} |
| 24 | | eqid 2737 |
. . . . . 6
⊢ ((𝑓 ↾ ∪ {𝑦
∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) = ((𝑓 ↾ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}) ∪ (◡𝑔 ↾ (𝑧 ∖ ∪ {𝑦 ∣ (𝑦 ⊆ 𝑧 ∧ (𝑔 “ (𝑤 ∖ (𝑓 “ 𝑦))) ⊆ (𝑧 ∖ 𝑦))}))) |
| 25 | | vex 3484 |
. . . . . 6
⊢ 𝑤 ∈ V |
| 26 | 15, 23, 24, 25 | sbthfilem 9238 |
. . . . 5
⊢ ((𝑤 ∈ Fin ∧ 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧) → 𝑧 ≈ 𝑤) |
| 27 | 8, 14, 26 | vtocl2g 3574 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
| 28 | 2, 3, 27 | syl2an 596 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
| 29 | 28 | 3adant1 1131 |
. 2
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)) |
| 30 | 29 | pm2.43i 52 |
1
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |