Description: Generalized partition-equivalence identification.
The partition-side scheme PetParts and the equivalence-side scheme PetErs define the same class of spans (pairs <. r , n >. ).
This plays the same organizational role for lifted spans that mpets plays for carriers: mpets identifies MembParts with CoMembErs at the membership-carrier level, while petseq identifies the corresponding span-level predicates built from Parts and Ers .
Unlike the earlier broad pets , the bridge used here is the type-safe span theorem typesafepets , which restricts to membership block-carriers. Since typedness ( r e. Rels and the appropriate carrier condition) is now built directly into PetParts and PetErs , this theorem can be used downstream without repeatedly re-establishing basic typing premises. (Contributed by Peter Mazsa, 19-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | petseq | ⊢ PetParts = PetErs |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | typesafepets | ⊢ ( ( 𝑛 ∈ MembParts ∧ 𝑟 ∈ V ) → ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ↔ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) ) | |
| 2 | 1 | elvd | ⊢ ( 𝑛 ∈ MembParts → ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ↔ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) ) |
| 3 | 2 | adantl | ⊢ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) → ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ↔ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) ) |
| 4 | 3 | pm5.32i | ⊢ ( ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) ↔ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) ) |
| 5 | mpets | ⊢ MembParts = CoMembErs | |
| 6 | 5 | eleq2i | ⊢ ( 𝑛 ∈ MembParts ↔ 𝑛 ∈ CoMembErs ) |
| 7 | 6 | anbi2i | ⊢ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ↔ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ) |
| 8 | 4 7 | bianbi | ⊢ ( ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) ↔ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) ) |
| 9 | 8 | opabbii | ⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) } = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) } |
| 10 | df-petparts | ⊢ PetParts = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) } | |
| 11 | df-peters | ⊢ PetErs = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) } | |
| 12 | 9 10 11 | 3eqtr4i | ⊢ PetParts = PetErs |