Metamath Proof Explorer

Theorem relop

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg , as funsng is to funop . (New usage is discouraged.)

Ref Expression
Hypotheses relop.1 ⊢ 𝐴 ∈ V
relop.2 ⊢ 𝐵 ∈ V
Assertion relop ( Rel ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) )

Proof

Step Hyp Ref Expression
1 relop.1 ⊢ 𝐴 ∈ V
2 relop.2 ⊢ 𝐵 ∈ V
3 df-rel ⊢ ( Rel ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) )
4 dfss2 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) ↔ ∀ 𝑧 ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝑧 ∈ ( V × V ) ) )
5 1 2 elop ⊢ ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑧 = { 𝐴 } ∨ 𝑧 = { 𝐴 , 𝐵 } ) )
6 elvv ⊢ ( 𝑧 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
7 5 6 imbi12i ⊢ ( ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝑧 ∈ ( V × V ) ) ↔ ( ( 𝑧 = { 𝐴 } ∨ 𝑧 = { 𝐴 , 𝐵 } ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
8 jaob ⊢ ( ( ( 𝑧 = { 𝐴 } ∨ 𝑧 = { 𝐴 , 𝐵 } ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
9 7 8 bitri ⊢ ( ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝑧 ∈ ( V × V ) ) ↔ ( ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
10 9 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝑧 ∈ ( V × V ) ) ↔ ∀ 𝑧 ( ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
11 19.26 ⊢ ( ∀ 𝑧 ( ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( ∀ 𝑧 ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∀ 𝑧 ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
12 10 11 bitri ⊢ ( ∀ 𝑧 ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝑧 ∈ ( V × V ) ) ↔ ( ∀ 𝑧 ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∀ 𝑧 ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
13 4 12 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) ↔ ( ∀ 𝑧 ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∀ 𝑧 ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
14 snex ⊢ { 𝐴 } ∈ V
15 eqeq1 ⊢ ( 𝑧 = { 𝐴 } → ( 𝑧 = { 𝐴 } ↔ { 𝐴 } = { 𝐴 } ) )
16 eqeq1 ⊢ ( 𝑧 = { 𝐴 } → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ { 𝐴 } = ⟨ 𝑥 , 𝑦 ⟩ ) )
17 eqcom ⊢ ( { 𝐴 } = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = { 𝐴 } )
18 vex ⊢ 𝑥 ∈ V
19 vex ⊢ 𝑦 ∈ V
20 18 19 opeqsn ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = { 𝐴 } ↔ ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) )
21 17 20 bitri ⊢ ( { 𝐴 } = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) )
22 16 21 bitrdi ⊢ ( 𝑧 = { 𝐴 } → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ) )
23 22 2exbidv ⊢ ( 𝑧 = { 𝐴 } → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ) )
24 15 23 imbi12d ⊢ ( 𝑧 = { 𝐴 } → ( ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( { 𝐴 } = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ) ) )
25 14 24 spcv ⊢ ( ∀ 𝑧 ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( { 𝐴 } = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ) )
26 sneq ⊢ ( 𝑤 = 𝑥 → { 𝑤 } = { 𝑥 } )
27 26 eqeq2d ⊢ ( 𝑤 = 𝑥 → ( 𝐴 = { 𝑤 } ↔ 𝐴 = { 𝑥 } ) )
28 27 cbvexvw ⊢ ( ∃ 𝑤 𝐴 = { 𝑤 } ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
29 ax6evr ⊢ ∃ 𝑦 𝑥 = 𝑦
30 19.41v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ↔ ( ∃ 𝑦 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) )
31 29 30 mpbiran ⊢ ( ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ↔ 𝐴 = { 𝑥 } )
32 31 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
33 eqid ⊢ { 𝐴 } = { 𝐴 }
34 33 a1bi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ↔ ( { 𝐴 } = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ) )
35 28 32 34 3bitr2ri ⊢ ( ( { 𝐴 } = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑦 ∧ 𝐴 = { 𝑥 } ) ) ↔ ∃ 𝑤 𝐴 = { 𝑤 } )
36 25 35 sylib ⊢ ( ∀ 𝑧 ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑤 𝐴 = { 𝑤 } )
37 eqid ⊢ { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 }
38 prex ⊢ { 𝐴 , 𝐵 } ∈ V
39 eqeq1 ⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( 𝑧 = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 } ) )
40 eqeq1 ⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ) )
41 40 2exbidv ⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ) )
42 39 41 imbi12d ⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
43 38 42 spcv ⊢ ( ∀ 𝑧 ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ) )
44 37 43 mpi ⊢ ( ∀ 𝑧 ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ )
45 eqcom ⊢ ( { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = { 𝐴 , 𝐵 } )
46 18 19 1 2 opeqpr ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = { 𝐴 , 𝐵 } ↔ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∨ ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐵 = { 𝑥 } ) ) )
47 45 46 bitri ⊢ ( { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∨ ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐵 = { 𝑥 } ) ) )
48 idd ⊢ ( 𝐴 = { 𝑤 } → ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
49 eqtr2 ⊢ ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 = { 𝑤 } ) → { 𝑥 , 𝑦 } = { 𝑤 } )
50 18 19 preqsn ⊢ ( { 𝑥 , 𝑦 } = { 𝑤 } ↔ ( 𝑥 = 𝑦 ∧ 𝑦 = 𝑤 ) )
51 50 simplbi ⊢ ( { 𝑥 , 𝑦 } = { 𝑤 } → 𝑥 = 𝑦 )
52 49 51 syl ⊢ ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 = { 𝑤 } ) → 𝑥 = 𝑦 )
53 dfsn2 ⊢ { 𝑥 } = { 𝑥 , 𝑥 }
54 preq2 ⊢ ( 𝑥 = 𝑦 → { 𝑥 , 𝑥 } = { 𝑥 , 𝑦 } )
55 53 54 eqtr2id ⊢ ( 𝑥 = 𝑦 → { 𝑥 , 𝑦 } = { 𝑥 } )
56 55 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 = { 𝑥 , 𝑦 } ↔ 𝐴 = { 𝑥 } ) )
57 53 54 eqtrid ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑥 , 𝑦 } )
58 57 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 = { 𝑥 } ↔ 𝐵 = { 𝑥 , 𝑦 } ) )
59 56 58 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐵 = { 𝑥 } ) ↔ ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
60 59 biimpd ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐵 = { 𝑥 } ) → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
61 60 expd ⊢ ( 𝑥 = 𝑦 → ( 𝐴 = { 𝑥 , 𝑦 } → ( 𝐵 = { 𝑥 } → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) ) )
62 61 com12 ⊢ ( 𝐴 = { 𝑥 , 𝑦 } → ( 𝑥 = 𝑦 → ( 𝐵 = { 𝑥 } → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) ) )
63 62 adantr ⊢ ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 = { 𝑤 } ) → ( 𝑥 = 𝑦 → ( 𝐵 = { 𝑥 } → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) ) )
64 52 63 mpd ⊢ ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐴 = { 𝑤 } ) → ( 𝐵 = { 𝑥 } → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
65 64 expcom ⊢ ( 𝐴 = { 𝑤 } → ( 𝐴 = { 𝑥 , 𝑦 } → ( 𝐵 = { 𝑥 } → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) ) )
66 65 impd ⊢ ( 𝐴 = { 𝑤 } → ( ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐵 = { 𝑥 } ) → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
67 48 66 jaod ⊢ ( 𝐴 = { 𝑤 } → ( ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∨ ( 𝐴 = { 𝑥 , 𝑦 } ∧ 𝐵 = { 𝑥 } ) ) → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
68 47 67 syl5bi ⊢ ( 𝐴 = { 𝑤 } → ( { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
69 68 2eximdv ⊢ ( 𝐴 = { 𝑤 } → ( ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
70 69 exlimiv ⊢ ( ∃ 𝑤 𝐴 = { 𝑤 } → ( ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ) )
71 70 imp ⊢ ( ( ∃ 𝑤 𝐴 = { 𝑤 } ∧ ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) )
72 36 44 71 syl2an ⊢ ( ( ∀ 𝑧 ( 𝑧 = { 𝐴 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ∀ 𝑧 ( 𝑧 = { 𝐴 , 𝐵 } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) )
73 13 72 sylbi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) )
74 simpr ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝑧 = { 𝐴 } ) → 𝑧 = { 𝐴 } )
75 equid ⊢ 𝑥 = 𝑥
76 75 jctl ⊢ ( 𝐴 = { 𝑥 } → ( 𝑥 = 𝑥 ∧ 𝐴 = { 𝑥 } ) )
77 18 18 opeqsn ⊢ ( ⟨ 𝑥 , 𝑥 ⟩ = { 𝐴 } ↔ ( 𝑥 = 𝑥 ∧ 𝐴 = { 𝑥 } ) )
78 76 77 sylibr ⊢ ( 𝐴 = { 𝑥 } → ⟨ 𝑥 , 𝑥 ⟩ = { 𝐴 } )
79 78 adantr ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝑧 = { 𝐴 } ) → ⟨ 𝑥 , 𝑥 ⟩ = { 𝐴 } )
80 74 79 eqtr4d ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝑧 = { 𝐴 } ) → 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ )
81 opeq12 ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑣 = 𝑥 ) → ⟨ 𝑤 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
82 81 eqeq2d ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑣 = 𝑥 ) → ( 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ) )
83 18 18 82 spc2ev ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
84 80 83 syl ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝑧 = { 𝐴 } ) → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
85 84 adantlr ⊢ ( ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∧ 𝑧 = { 𝐴 } ) → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
86 preq12 ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → { 𝐴 , 𝐵 } = { { 𝑥 } , { 𝑥 , 𝑦 } } )
87 86 eqeq2d ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → ( 𝑧 = { 𝐴 , 𝐵 } ↔ 𝑧 = { { 𝑥 } , { 𝑥 , 𝑦 } } ) )
88 87 biimpa ⊢ ( ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∧ 𝑧 = { 𝐴 , 𝐵 } ) → 𝑧 = { { 𝑥 } , { 𝑥 , 𝑦 } } )
89 18 19 dfop ⊢ ⟨ 𝑥 , 𝑦 ⟩ = { { 𝑥 } , { 𝑥 , 𝑦 } }
90 88 89 eqtr4di ⊢ ( ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∧ 𝑧 = { 𝐴 , 𝐵 } ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
91 opeq12 ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ⟨ 𝑤 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
92 91 eqeq2d ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
93 18 19 92 spc2ev ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
94 90 93 syl ⊢ ( ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∧ 𝑧 = { 𝐴 , 𝐵 } ) → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
95 85 94 jaodan ⊢ ( ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) ∧ ( 𝑧 = { 𝐴 } ∨ 𝑧 = { 𝐴 , 𝐵 } ) ) → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
96 95 ex ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → ( ( 𝑧 = { 𝐴 } ∨ 𝑧 = { 𝐴 , 𝐵 } ) → ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ ) )
97 elvv ⊢ ( 𝑧 ∈ ( V × V ) ↔ ∃ 𝑤 ∃ 𝑣 𝑧 = ⟨ 𝑤 , 𝑣 ⟩ )
98 96 5 97 3imtr4g ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → ( 𝑧 ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝑧 ∈ ( V × V ) ) )
99 98 ssrdv ⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) )
100 99 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) → ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) )
101 73 100 impbii ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ⊆ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) )
102 3 101 bitri ⊢ ( Rel ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑥 , 𝑦 } ) )