| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elxp2 5708 | . . . 4
⊢ (𝑝 ∈ (𝐴 × 𝐵) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑝 = 〈𝑎, 𝑏〉) | 
| 2 |  | xpord2.1 | . . . . . . . . 9
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} | 
| 3 | 2 | xpord2pred 8171 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})) | 
| 4 | 3 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})) | 
| 5 |  | sexp2.1 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 Se 𝐴) | 
| 6 |  | setlikespec 6345 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑎) ∈ V) | 
| 7 | 6 | ancoms 458 | . . . . . . . . . . . 12
⊢ ((𝑅 Se 𝐴 ∧ 𝑎 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑎) ∈ V) | 
| 8 | 5, 7 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑎) ∈ V) | 
| 9 | 8 | adantrr 717 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Pred(𝑅, 𝐴, 𝑎) ∈ V) | 
| 10 |  | vsnex 5433 | . . . . . . . . . . 11
⊢ {𝑎} ∈ V | 
| 11 | 10 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → {𝑎} ∈ V) | 
| 12 | 9, 11 | unexd 7775 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∈ V) | 
| 13 |  | sexp2.2 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 Se 𝐵) | 
| 14 |  | setlikespec 6345 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑆 Se 𝐵) → Pred(𝑆, 𝐵, 𝑏) ∈ V) | 
| 15 | 14 | ancoms 458 | . . . . . . . . . . . 12
⊢ ((𝑆 Se 𝐵 ∧ 𝑏 ∈ 𝐵) → Pred(𝑆, 𝐵, 𝑏) ∈ V) | 
| 16 | 13, 15 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → Pred(𝑆, 𝐵, 𝑏) ∈ V) | 
| 17 | 16 | adantrl 716 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Pred(𝑆, 𝐵, 𝑏) ∈ V) | 
| 18 |  | vsnex 5433 | . . . . . . . . . . 11
⊢ {𝑏} ∈ V | 
| 19 | 18 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → {𝑏} ∈ V) | 
| 20 | 17, 19 | unexd 7775 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∈ V) | 
| 21 | 12, 20 | xpexd 7772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∈ V) | 
| 22 | 21 | difexd 5330 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ∈ V) | 
| 23 | 4, 22 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ∈ V) | 
| 24 |  | predeq3 6324 | . . . . . . 7
⊢ (𝑝 = 〈𝑎, 𝑏〉 → Pred(𝑇, (𝐴 × 𝐵), 𝑝) = Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉)) | 
| 25 | 24 | eleq1d 2825 | . . . . . 6
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (Pred(𝑇, (𝐴 × 𝐵), 𝑝) ∈ V ↔ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ∈ V)) | 
| 26 | 23, 25 | syl5ibrcom 247 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑝 = 〈𝑎, 𝑏〉 → Pred(𝑇, (𝐴 × 𝐵), 𝑝) ∈ V)) | 
| 27 | 26 | rexlimdvva 3212 | . . . 4
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑝 = 〈𝑎, 𝑏〉 → Pred(𝑇, (𝐴 × 𝐵), 𝑝) ∈ V)) | 
| 28 | 1, 27 | biimtrid 242 | . . 3
⊢ (𝜑 → (𝑝 ∈ (𝐴 × 𝐵) → Pred(𝑇, (𝐴 × 𝐵), 𝑝) ∈ V)) | 
| 29 | 28 | ralrimiv 3144 | . 2
⊢ (𝜑 → ∀𝑝 ∈ (𝐴 × 𝐵)Pred(𝑇, (𝐴 × 𝐵), 𝑝) ∈ V) | 
| 30 |  | dfse3 6356 | . 2
⊢ (𝑇 Se (𝐴 × 𝐵) ↔ ∀𝑝 ∈ (𝐴 × 𝐵)Pred(𝑇, (𝐴 × 𝐵), 𝑝) ∈ V) | 
| 31 | 29, 30 | sylibr 234 | 1
⊢ (𝜑 → 𝑇 Se (𝐴 × 𝐵)) |