This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem or2expropbilem1

Description: Lemma 1 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion or2expropbilem1 ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑎 ∈ V
2 vex ⊢ 𝑏 ∈ V
3 1 2 pm3.2i ⊢ ( 𝑎 ∈ V ∧ 𝑏 ∈ V )
4 3 a1i ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) )
5 4 anim1ci ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝜑 ) → ( 𝜑 ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) )
6 5 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝜑 ) ∧ ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ) → ( 𝜑 ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) )
7 sbcid ⊢ ( [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑎 ] 𝜑 )
8 sbcid ⊢ ( [ 𝑎 / 𝑎 ] 𝜑 ↔ 𝜑 )
9 7 8 sylbbr ⊢ ( 𝜑 → [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 )
10 9 adantl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝜑 ) → [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 )
11 opeq12 ⊢ ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
12 10 11 anim12ci ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝜑 ) ∧ ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ) )
13 nfv ⊢ Ⅎ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 )
14 nfv ⊢ Ⅎ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 )
15 opeq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
16 15 eqeq2d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
17 dfsbcq ⊢ ( 𝑦 = 𝑏 → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
18 dfsbcq ⊢ ( 𝑥 = 𝑎 → ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑎 / 𝑎 ] 𝜑 ) )
19 18 sbcbidv ⊢ ( 𝑥 = 𝑎 → ( [ 𝑏 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ) )
20 17 19 sylan9bbr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ) )
21 16 20 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ) ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ) ) )
23 13 14 22 spc2ed ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ [ 𝑏 / 𝑏 ] [ 𝑎 / 𝑎 ] 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) )
24 6 12 23 sylc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝜑 ) ∧ ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
25 24 exp31 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝜑 → ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )
26 25 com23 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 = 𝑎 ∧ 𝐵 = 𝑏 ) → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )