Metamath Proof Explorer

Theorem prelrrx2b

Description: An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023)

Ref Expression
Hypotheses prelrrx2.i ⊢ 𝐼 = { 1 , 2 }
prelrrx2.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion prelrrx2b ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) ↔ 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } ) )

Proof

Step Hyp Ref Expression
1 prelrrx2.i ⊢ 𝐼 = { 1 , 2 }
2 prelrrx2.b ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3 2 eleq2i ⊢ ( 𝑍 ∈ 𝑃 ↔ 𝑍 ∈ ( ℝ ↑m 𝐼 ) )
4 1 oveq2i ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m { 1 , 2 } )
5 4 eleq2i ⊢ ( 𝑍 ∈ ( ℝ ↑m 𝐼 ) ↔ 𝑍 ∈ ( ℝ ↑m { 1 , 2 } ) )
6 3 5 bitri ⊢ ( 𝑍 ∈ 𝑃 ↔ 𝑍 ∈ ( ℝ ↑m { 1 , 2 } ) )
7 elmapi ⊢ ( 𝑍 ∈ ( ℝ ↑m { 1 , 2 } ) → 𝑍 : { 1 , 2 } ⟶ ℝ )
8 1ne2 ⊢ 1 ≠ 2
9 1ex ⊢ 1 ∈ V
10 2ex ⊢ 2 ∈ V
11 9 10 fprb ⊢ ( 1 ≠ 2 → ( 𝑍 : { 1 , 2 } ⟶ ℝ ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) )
12 8 11 ax-mp ⊢ ( 𝑍 : { 1 , 2 } ⟶ ℝ ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } )
13 fveq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( 𝑍 ‘ 1 ) = ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 1 ) )
14 vex ⊢ 𝑥 ∈ V
15 9 14 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 1 ) = 𝑥 )
16 8 15 ax-mp ⊢ ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 1 ) = 𝑥
17 13 16 eqtrdi ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( 𝑍 ‘ 1 ) = 𝑥 )
18 17 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( 𝑍 ‘ 1 ) = 𝐴 ↔ 𝑥 = 𝐴 ) )
19 fveq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( 𝑍 ‘ 2 ) = ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 2 ) )
20 vex ⊢ 𝑦 ∈ V
21 10 20 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 2 ) = 𝑦 )
22 8 21 ax-mp ⊢ ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 2 ) = 𝑦
23 19 22 eqtrdi ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( 𝑍 ‘ 2 ) = 𝑦 )
24 23 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( 𝑍 ‘ 2 ) = 𝐵 ↔ 𝑦 = 𝐵 ) )
25 18 24 anbi12d ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
26 25 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
27 opeq2 ⊢ ( 𝑥 = 𝐴 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝐴 ⟩ )
28 27 adantr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝐴 ⟩ )
29 opeq2 ⊢ ( 𝑦 = 𝐵 → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝐵 ⟩ )
30 29 adantl ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝐵 ⟩ )
31 28 30 preq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } )
32 31 eqeq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ↔ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) )
33 32 biimpcd ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) )
34 33 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) )
35 26 34 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) )
36 35 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) ) )
37 36 rexlimdvva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) ) )
38 12 37 biimtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 : { 1 , 2 } ⟶ ℝ → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) ) )
39 7 38 syl5 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 ∈ ( ℝ ↑m { 1 , 2 } ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) ) )
40 6 39 biimtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 ∈ 𝑃 → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) ) )
41 40 imp ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 ∈ 𝑃 ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) → 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) )
42 17 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( 𝑍 ‘ 1 ) = 𝑋 ↔ 𝑥 = 𝑋 ) )
43 23 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( 𝑍 ‘ 2 ) = 𝑌 ↔ 𝑦 = 𝑌 ) )
44 42 43 anbi12d ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) )
45 44 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) )
46 opeq2 ⊢ ( 𝑥 = 𝑋 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑋 ⟩ )
47 46 adantr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑋 ⟩ )
48 opeq2 ⊢ ( 𝑦 = 𝑌 → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝑌 ⟩ )
49 48 adantl ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝑌 ⟩ )
50 47 49 preq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } )
51 50 eqeq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ↔ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
52 51 biimpcd ⊢ ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
53 52 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
54 45 53 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
55 54 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
56 55 rexlimdvva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
57 12 56 biimtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 : { 1 , 2 } ⟶ ℝ → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
58 7 57 syl5 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 ∈ ( ℝ ↑m { 1 , 2 } ) → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
59 6 58 biimtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 ∈ 𝑃 → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
60 59 imp ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 ∈ 𝑃 ) → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) → 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
61 41 60 orim12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 ∈ 𝑃 ) → ( ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) → ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∨ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
62 61 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 ∈ 𝑃 ) ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) → ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∨ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
63 elprg ⊢ ( 𝑍 ∈ 𝑃 → ( 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } ↔ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∨ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
64 63 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 ∈ 𝑃 ) ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) → ( 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } ↔ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∨ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) ) )
65 62 64 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 ∈ 𝑃 ) ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) → 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } )
66 65 expl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) → 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } ) )
67 elpri ⊢ ( 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } → ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∨ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) )
68 1 2 prelrrx2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 )
69 68 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 )
70 eleq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( 𝑍 ∈ 𝑃 ↔ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 ) )
71 70 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → ( 𝑍 ∈ 𝑃 ↔ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 ) )
72 69 71 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → 𝑍 ∈ 𝑃 )
73 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
74 8 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 1 ≠ 2 )
75 fvpr1g ⊢ ( ( 1 ∈ V ∧ 𝐴 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 )
76 9 73 74 75 mp3an2i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 )
77 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
78 fvpr2g ⊢ ( ( 2 ∈ V ∧ 𝐵 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 )
79 10 77 74 78 mp3an2i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 )
80 76 79 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 ∧ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 ) )
81 80 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 ∧ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 ) )
82 fveq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( 𝑍 ‘ 1 ) = ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) )
83 82 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( ( 𝑍 ‘ 1 ) = 𝐴 ↔ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 ) )
84 fveq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( 𝑍 ‘ 2 ) = ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) )
85 84 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( ( 𝑍 ‘ 2 ) = 𝐵 ↔ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 ) )
86 83 85 anbi12d ⊢ ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ↔ ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 ∧ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 ) ) )
87 86 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ↔ ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 1 ) = 𝐴 ∧ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ‘ 2 ) = 𝐵 ) ) )
88 81 87 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) )
89 88 orcd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) )
90 72 89 jca ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ) → ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) )
91 90 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } → ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) ) )
92 1 2 prelrrx2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∈ 𝑃 )
93 92 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∈ 𝑃 )
94 eleq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( 𝑍 ∈ 𝑃 ↔ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∈ 𝑃 ) )
95 94 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( 𝑍 ∈ 𝑃 ↔ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ∈ 𝑃 ) )
96 93 95 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → 𝑍 ∈ 𝑃 )
97 simpl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → 𝑋 ∈ ℝ )
98 8 a1i ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → 1 ≠ 2 )
99 fvpr1g ⊢ ( ( 1 ∈ V ∧ 𝑋 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 )
100 9 97 98 99 mp3an2i ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 )
101 simpr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → 𝑌 ∈ ℝ )
102 fvpr2g ⊢ ( ( 2 ∈ V ∧ 𝑌 ∈ ℝ ∧ 1 ≠ 2 ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 )
103 10 101 98 102 mp3an2i ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 )
104 100 103 jca ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 ∧ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 ) )
105 104 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 ∧ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 ) )
106 fveq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( 𝑍 ‘ 1 ) = ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) )
107 106 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( ( 𝑍 ‘ 1 ) = 𝑋 ↔ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 ) )
108 fveq1 ⊢ ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( 𝑍 ‘ 2 ) = ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) )
109 108 eqeq1d ⊢ ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( ( 𝑍 ‘ 2 ) = 𝑌 ↔ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 ) )
110 107 109 anbi12d ⊢ ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ↔ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 ∧ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 ) ) )
111 110 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ↔ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 1 ) = 𝑋 ∧ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ‘ 2 ) = 𝑌 ) ) )
112 105 111 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) )
113 112 olcd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) )
114 96 113 jca ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) )
115 114 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } → ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) ) )
116 91 115 jaod ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∨ 𝑍 = { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } ) → ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) ) )
117 67 116 syl5 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } → ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) ) )
118 66 117 impbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 1 ) = 𝐴 ∧ ( 𝑍 ‘ 2 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 1 ) = 𝑋 ∧ ( 𝑍 ‘ 2 ) = 𝑌 ) ) ) ↔ 𝑍 ∈ { { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } , { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ } } ) )