Theorem sexp2

Description: Condition for the relationship in frxp2 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	xpord2.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
	sexp2.1	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
	sexp2.2	⊢ ( 𝜑 → 𝑆 Se 𝐵 )
Assertion	sexp2	⊢ ( 𝜑 → 𝑇 Se ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpord2.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2		sexp2.1	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
3		sexp2.2	⊢ ( 𝜑 → 𝑆 Se 𝐵 )
4		elxp2	⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ )
5	1	xpord2pred	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
6	5	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
7		setlikespec	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ∈ V )
8	7	ancoms	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑎 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ∈ V )
9	2 8	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ∈ V )
10	9	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ∈ V )
11		snex	⊢ { 𝑎 } ∈ V
12	11	a1i	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → { 𝑎 } ∈ V )
13	10 12	unexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∈ V )
14		setlikespec	⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑆 Se 𝐵 ) → Pred ( 𝑆 , 𝐵 , 𝑏 ) ∈ V )
15	14	ancoms	⊢ ( ( 𝑆 Se 𝐵 ∧ 𝑏 ∈ 𝐵 ) → Pred ( 𝑆 , 𝐵 , 𝑏 ) ∈ V )
16	3 15	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Pred ( 𝑆 , 𝐵 , 𝑏 ) ∈ V )
17	16	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → Pred ( 𝑆 , 𝐵 , 𝑏 ) ∈ V )
18		snex	⊢ { 𝑏 } ∈ V
19	18	a1i	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → { 𝑏 } ∈ V )
20	17 19	unexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∈ V )
21	13 20	xpexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∈ V )
22	21	difexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∈ V )
23	6 22	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ∈ V )
24		predeq3	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) = Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) )
25	24	eleq1d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) ∈ V ↔ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ∈ V ) )
26	23 25	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) ∈ V ) )
27	26	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) ∈ V ) )
28	4 27	syl5bi	⊢ ( 𝜑 → ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) ∈ V ) )
29	28	ralrimiv	⊢ ( 𝜑 → ∀ 𝑝 ∈ ( 𝐴 × 𝐵 ) Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) ∈ V )
30		dfse3	⊢ ( 𝑇 Se ( 𝐴 × 𝐵 ) ↔ ∀ 𝑝 ∈ ( 𝐴 × 𝐵 ) Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , 𝑝 ) ∈ V )
31	29 30	sylibr	⊢ ( 𝜑 → 𝑇 Se ( 𝐴 × 𝐵 ) )