copsex2b

Description: Biconditional form of copsex2d . TODO: prove a relative version, that is, with E. x e. V E. y e. W ... ( A e. V /\ B e. W ) . (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Hypotheses	copsex2b.xph	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	copsex2b.yph	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
	copsex2b.xch	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	copsex2b.ych	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
	copsex2b.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	copsex2b	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		copsex2b.xph	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		copsex2b.yph	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3		copsex2b.xch	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
4		copsex2b.ych	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
5		copsex2b.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
6		eqcom	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	opth	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
10	6 9	bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
11		eqvisset	⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )
12		eqvisset	⊢ ( 𝑦 = 𝐵 → 𝐵 ∈ V )
13	11 12	anim12i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
14	10 13	sylbi	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
15	14	adantr	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
16	15	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
17	16	anim2i	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) → ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
18		simpl	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
19	18	anim2i	⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) → ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
20		ax-5	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∀ 𝑥 ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
21	1 20	hban	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ∀ 𝑥 ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
22		ax-5	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∀ 𝑦 ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
23	2 22	hban	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ∀ 𝑦 ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
24	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → Ⅎ 𝑥 𝜒 )
25	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → Ⅎ 𝑦 𝜒 )
26		simprl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → 𝐴 ∈ V )
27		simprr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → 𝐵 ∈ V )
28	5	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
29	21 23 24 25 26 27 28	copsex2d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ 𝜒 ) )
30		ibar	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝜒 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 𝜒 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )
32	29 31	bitrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )
33	17 19 32	pm5.21nd	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) ) )

Metamath Proof Explorer

Theorem copsex2b

Proof