Metamath Proof Explorer

Theorem xpdifid

Description: The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Assertion xpdifid ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) = ( ( 𝐴 × 𝐵 ) ∖ I )

Proof

Step Hyp Ref Expression
1 elxp ⊢ ( 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
2 1 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
3 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ∃ 𝑖 ∃ 𝑥 ∈ 𝐴 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
4 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
5 4 exbii ⊢ ( ∃ 𝑖 ∃ 𝑥 ∈ 𝐴 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
6 2 3 5 3bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) ↔ ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
7 eliun ⊢ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) )
8 eldif ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ↔ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ¬ ⟨ 𝑖 , 𝑗 ⟩ ∈ I ) )
9 opelxp ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) )
10 df-br ⊢ ( 𝑖 I 𝑗 ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ I )
11 vex ⊢ 𝑗 ∈ V
12 11 ideq ⊢ ( 𝑖 I 𝑗 ↔ 𝑖 = 𝑗 )
13 10 12 bitr3i ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ I ↔ 𝑖 = 𝑗 )
14 13 necon3bbii ⊢ ( ¬ ⟨ 𝑖 , 𝑗 ⟩ ∈ I ↔ 𝑖 ≠ 𝑗 )
15 9 14 anbi12i ⊢ ( ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ¬ ⟨ 𝑖 , 𝑗 ⟩ ∈ I ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) )
16 8 15 bitri ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) )
17 16 anbi2i ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) ) )
18 17 2exbii ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) ) )
19 eldifi ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → 𝑝 ∈ ( 𝐴 × 𝐵 ) )
20 elxpi ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) )
21 simpl ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ )
22 21 2eximi ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ )
23 19 20 22 3syl ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ )
24 23 ancli ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) )
25 19.42vv ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) )
26 24 25 sylibr ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ∃ 𝑖 ∃ 𝑗 ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) )
27 ancom ⊢ ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) )
28 eleq1 ⊢ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) )
29 28 adantl ⊢ ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) )
30 29 pm5.32da ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) ) )
31 27 30 bitrid ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) ) )
32 31 2exbidv ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) ) )
33 26 32 mpbid ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) → ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) )
34 28 biimpar ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) → 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) )
35 34 exlimivv ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) → 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) )
36 33 35 impbii ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ) )
37 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
38 simprl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑖 ∈ { 𝑦 } )
39 velsn ⊢ ( 𝑖 ∈ { 𝑦 } ↔ 𝑖 = 𝑦 )
40 38 39 sylib ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑖 = 𝑦 )
41 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑦 ∈ 𝐴 )
42 40 41 eqeltrd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑖 ∈ 𝐴 )
43 simprr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) )
44 43 eldifad ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑗 ∈ 𝐵 )
45 43 eldifbd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → ¬ 𝑗 ∈ { 𝑦 } )
46 velsn ⊢ ( 𝑗 ∈ { 𝑦 } ↔ 𝑗 = 𝑦 )
47 46 necon3bbii ⊢ ( ¬ 𝑗 ∈ { 𝑦 } ↔ 𝑗 ≠ 𝑦 )
48 45 47 sylib ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑗 ≠ 𝑦 )
49 48 necomd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑦 ≠ 𝑗 )
50 40 49 eqnetrd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → 𝑖 ≠ 𝑗 )
51 42 44 50 jca31 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) )
52 51 adantll ⊢ ( ( ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) )
53 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
54 53 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑖 ∈ { 𝑥 } ↔ 𝑖 ∈ { 𝑦 } ) )
55 53 difeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑦 } ) )
56 55 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ↔ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) )
57 54 56 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ↔ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) ) )
58 57 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) )
59 58 biimpi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑦 } ) ) )
60 52 59 r19.29a ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) )
61 simpll ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ∈ 𝐴 )
62 vsnid ⊢ 𝑖 ∈ { 𝑖 }
63 62 a1i ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ∈ { 𝑖 } )
64 simplr ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑗 ∈ 𝐵 )
65 simpr ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ≠ 𝑗 )
66 65 necomd ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑗 ≠ 𝑖 )
67 velsn ⊢ ( 𝑗 ∈ { 𝑖 } ↔ 𝑗 = 𝑖 )
68 67 necon3bbii ⊢ ( ¬ 𝑗 ∈ { 𝑖 } ↔ 𝑗 ≠ 𝑖 )
69 66 68 sylibr ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → ¬ 𝑗 ∈ { 𝑖 } )
70 64 69 eldifd ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑗 ∈ ( 𝐵 ∖ { 𝑖 } ) )
71 sneq ⊢ ( 𝑥 = 𝑖 → { 𝑥 } = { 𝑖 } )
72 71 eleq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑖 ∈ { 𝑥 } ↔ 𝑖 ∈ { 𝑖 } ) )
73 71 difeq2d ⊢ ( 𝑥 = 𝑖 → ( 𝐵 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑖 } ) )
74 73 eleq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ↔ 𝑗 ∈ ( 𝐵 ∖ { 𝑖 } ) ) )
75 72 74 anbi12d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ↔ ( 𝑖 ∈ { 𝑖 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑖 } ) ) ) )
76 75 rspcev ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑖 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑖 } ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) )
77 61 63 70 76 syl12anc ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) → ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) )
78 60 77 impbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) )
79 78 anbi2i ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) ) )
80 37 79 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) ) )
81 80 2exbii ⊢ ( ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑖 ≠ 𝑗 ) ) )
82 18 36 81 3bitr4i ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) ↔ ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) )
83 6 7 82 3bitr4i ⊢ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) ↔ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ I ) )
84 83 eqriv ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ { 𝑥 } ) ) = ( ( 𝐴 × 𝐵 ) ∖ I )