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 ( ( 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 = 𝑎𝐵 = 𝑏 ) → ( 𝜑 → ∃ 𝑥𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) ) )