Description: Disjointness is absolute for transitive models. Compare Example I.16.3 of Kunen2 p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | disjabso | |- ( ( Tr M /\ A e. M ) -> ( ( A i^i B ) = (/) <-> A. x e. M ( x e. A -> -. x e. B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | disj | |- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B ) |
|
| 2 | ralabso | |- ( ( Tr M /\ A e. M ) -> ( A. x e. A -. x e. B <-> A. x e. M ( x e. A -> -. x e. B ) ) ) |
|
| 3 | 1 2 | bitrid | |- ( ( Tr M /\ A e. M ) -> ( ( A i^i B ) = (/) <-> A. x e. M ( x e. A -> -. x e. B ) ) ) |