Metamath Proof Explorer

Theorem brapply

Description: Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypotheses brapply.1 ⊢ 𝐴 ∈ V
brapply.2 ⊢ 𝐵 ∈ V
brapply.3 ⊢ 𝐶 ∈ V
Assertion brapply ( ⟨ 𝐴 , 𝐵 ⟩ Apply 𝐶 ↔ 𝐶 = ( 𝐴 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 brapply.1 ⊢ 𝐴 ∈ V
2 brapply.2 ⊢ 𝐵 ∈ V
3 brapply.3 ⊢ 𝐶 ∈ V
4 snex ⊢ { ( 𝐴 “ { 𝐵 } ) } ∈ V
5 4 inex1 ⊢ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ∈ V
6 unieq ⊢ ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) → ∪ 𝑥 = ∪ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
7 6 unieqd ⊢ ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) → ∪ ∪ 𝑥 = ∪ ∪ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
8 7 eqeq2d ⊢ ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) → ( 𝐶 = ∪ ∪ 𝑥 ↔ 𝐶 = ∪ ∪ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ) )
9 5 8 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ∧ 𝐶 = ∪ ∪ 𝑥 ) ↔ 𝐶 = ∪ ∪ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
10 df-apply ⊢ Apply = ( ( Bigcup ∘ Bigcup ) ∘ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) )
11 10 breqi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Apply 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ ( ( Bigcup ∘ Bigcup ) ∘ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) ) 𝐶 )
12 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
13 12 3 brco ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( Bigcup ∘ Bigcup ) ∘ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) ) 𝐶 ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) 𝑥 ∧ 𝑥 ( Bigcup ∘ Bigcup ) 𝐶 ) )
14 vex ⊢ 𝑥 ∈ V
15 12 14 brco ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) 𝑥 ↔ ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) 𝑦 ∧ 𝑦 ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) 𝑥 ) )
16 vex ⊢ 𝑦 ∈ V
17 12 16 brco ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) 𝑦 ↔ ∃ 𝑧 ( ⟨ 𝐴 , 𝐵 ⟩ pprod ( I , Singleton ) 𝑧 ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) )
18 vex ⊢ 𝑧 ∈ V
19 1 2 18 brpprod3a ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ pprod ( I , Singleton ) 𝑧 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐵 Singleton 𝑏 ) )
20 3anrot ⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐵 Singleton 𝑏 ) ↔ ( 𝐴 I 𝑎 ∧ 𝐵 Singleton 𝑏 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
21 vex ⊢ 𝑎 ∈ V
22 21 ideq ⊢ ( 𝐴 I 𝑎 ↔ 𝐴 = 𝑎 )
23 eqcom ⊢ ( 𝐴 = 𝑎 ↔ 𝑎 = 𝐴 )
24 22 23 bitri ⊢ ( 𝐴 I 𝑎 ↔ 𝑎 = 𝐴 )
25 vex ⊢ 𝑏 ∈ V
26 2 25 brsingle ⊢ ( 𝐵 Singleton 𝑏 ↔ 𝑏 = { 𝐵 } )
27 biid ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ )
28 24 26 27 3anbi123i ⊢ ( ( 𝐴 I 𝑎 ∧ 𝐵 Singleton 𝑏 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐵 } ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
29 20 28 bitri ⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐵 Singleton 𝑏 ) ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐵 } ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
30 29 2exbii ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝐴 I 𝑎 ∧ 𝐵 Singleton 𝑏 ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐵 } ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
31 snex ⊢ { 𝐵 } ∈ V
32 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
33 32 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝐴 , 𝑏 ⟩ ) )
34 opeq2 ⊢ ( 𝑏 = { 𝐵 } → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , { 𝐵 } ⟩ )
35 34 eqeq2d ⊢ ( 𝑏 = { 𝐵 } → ( 𝑧 = ⟨ 𝐴 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ ) )
36 1 31 33 35 ceqsex2v ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝐴 ∧ 𝑏 = { 𝐵 } ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ )
37 19 30 36 3bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ pprod ( I , Singleton ) 𝑧 ↔ 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ )
38 37 anbi1i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ pprod ( I , Singleton ) 𝑧 ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) ↔ ( 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) )
39 38 exbii ⊢ ( ∃ 𝑧 ( ⟨ 𝐴 , 𝐵 ⟩ pprod ( I , Singleton ) 𝑧 ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) )
40 opex ⊢ ⟨ 𝐴 , { 𝐵 } ⟩ ∈ V
41 breq1 ⊢ ( 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ → ( 𝑧 ( Singleton ∘ Img ) 𝑦 ↔ ⟨ 𝐴 , { 𝐵 } ⟩ ( Singleton ∘ Img ) 𝑦 ) )
42 40 41 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) ↔ ⟨ 𝐴 , { 𝐵 } ⟩ ( Singleton ∘ Img ) 𝑦 )
43 40 16 brco ⊢ ( ⟨ 𝐴 , { 𝐵 } ⟩ ( Singleton ∘ Img ) 𝑦 ↔ ∃ 𝑥 ( ⟨ 𝐴 , { 𝐵 } ⟩ Img 𝑥 ∧ 𝑥 Singleton 𝑦 ) )
44 1 31 14 brimg ⊢ ( ⟨ 𝐴 , { 𝐵 } ⟩ Img 𝑥 ↔ 𝑥 = ( 𝐴 “ { 𝐵 } ) )
45 14 16 brsingle ⊢ ( 𝑥 Singleton 𝑦 ↔ 𝑦 = { 𝑥 } )
46 44 45 anbi12i ⊢ ( ( ⟨ 𝐴 , { 𝐵 } ⟩ Img 𝑥 ∧ 𝑥 Singleton 𝑦 ) ↔ ( 𝑥 = ( 𝐴 “ { 𝐵 } ) ∧ 𝑦 = { 𝑥 } ) )
47 46 exbii ⊢ ( ∃ 𝑥 ( ⟨ 𝐴 , { 𝐵 } ⟩ Img 𝑥 ∧ 𝑥 Singleton 𝑦 ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝐴 “ { 𝐵 } ) ∧ 𝑦 = { 𝑥 } ) )
48 1 imaex ⊢ ( 𝐴 “ { 𝐵 } ) ∈ V
49 sneq ⊢ ( 𝑥 = ( 𝐴 “ { 𝐵 } ) → { 𝑥 } = { ( 𝐴 “ { 𝐵 } ) } )
50 49 eqeq2d ⊢ ( 𝑥 = ( 𝐴 “ { 𝐵 } ) → ( 𝑦 = { 𝑥 } ↔ 𝑦 = { ( 𝐴 “ { 𝐵 } ) } ) )
51 48 50 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝐴 “ { 𝐵 } ) ∧ 𝑦 = { 𝑥 } ) ↔ 𝑦 = { ( 𝐴 “ { 𝐵 } ) } )
52 47 51 bitri ⊢ ( ∃ 𝑥 ( ⟨ 𝐴 , { 𝐵 } ⟩ Img 𝑥 ∧ 𝑥 Singleton 𝑦 ) ↔ 𝑦 = { ( 𝐴 “ { 𝐵 } ) } )
53 42 43 52 3bitri ⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝐴 , { 𝐵 } ⟩ ∧ 𝑧 ( Singleton ∘ Img ) 𝑦 ) ↔ 𝑦 = { ( 𝐴 “ { 𝐵 } ) } )
54 17 39 53 3bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) 𝑦 ↔ 𝑦 = { ( 𝐴 “ { 𝐵 } ) } )
55 eqid ⊢ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) )
56 brxp ⊢ ( 𝑦 ( V × V ) 𝑥 ↔ ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) )
57 16 14 56 mpbir2an ⊢ 𝑦 ( V × V ) 𝑥
58 epel ⊢ ( 𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦 )
59 58 anbi1ci ⊢ ( ( 𝑧 ∈ Singletons ∧ 𝑧 E 𝑦 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ Singletons ) )
60 16 brresi ⊢ ( 𝑧 ( E ↾ Singletons ) 𝑦 ↔ ( 𝑧 ∈ Singletons ∧ 𝑧 E 𝑦 ) )
61 elin ⊢ ( 𝑧 ∈ ( 𝑦 ∩ Singletons ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ Singletons ) )
62 59 60 61 3bitr4ri ⊢ ( 𝑧 ∈ ( 𝑦 ∩ Singletons ) ↔ 𝑧 ( E ↾ Singletons ) 𝑦 )
63 16 14 55 57 62 brtxpsd3 ⊢ ( 𝑦 ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) 𝑥 ↔ 𝑥 = ( 𝑦 ∩ Singletons ) )
64 54 63 anbi12i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) 𝑦 ∧ 𝑦 ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) 𝑥 ) ↔ ( 𝑦 = { ( 𝐴 “ { 𝐵 } ) } ∧ 𝑥 = ( 𝑦 ∩ Singletons ) ) )
65 64 exbii ⊢ ( ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) 𝑦 ∧ 𝑦 ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 = { ( 𝐴 “ { 𝐵 } ) } ∧ 𝑥 = ( 𝑦 ∩ Singletons ) ) )
66 ineq1 ⊢ ( 𝑦 = { ( 𝐴 “ { 𝐵 } ) } → ( 𝑦 ∩ Singletons ) = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
67 66 eqeq2d ⊢ ( 𝑦 = { ( 𝐴 “ { 𝐵 } ) } → ( 𝑥 = ( 𝑦 ∩ Singletons ) ↔ 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ) )
68 4 67 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = { ( 𝐴 “ { 𝐵 } ) } ∧ 𝑥 = ( 𝑦 ∩ Singletons ) ) ↔ 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
69 15 65 68 3bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) 𝑥 ↔ 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
70 14 3 brco ⊢ ( 𝑥 ( Bigcup ∘ Bigcup ) 𝐶 ↔ ∃ 𝑦 ( 𝑥 Bigcup 𝑦 ∧ 𝑦 Bigcup 𝐶 ) )
71 16 brbigcup ⊢ ( 𝑥 Bigcup 𝑦 ↔ ∪ 𝑥 = 𝑦 )
72 eqcom ⊢ ( ∪ 𝑥 = 𝑦 ↔ 𝑦 = ∪ 𝑥 )
73 71 72 bitri ⊢ ( 𝑥 Bigcup 𝑦 ↔ 𝑦 = ∪ 𝑥 )
74 3 brbigcup ⊢ ( 𝑦 Bigcup 𝐶 ↔ ∪ 𝑦 = 𝐶 )
75 eqcom ⊢ ( ∪ 𝑦 = 𝐶 ↔ 𝐶 = ∪ 𝑦 )
76 74 75 bitri ⊢ ( 𝑦 Bigcup 𝐶 ↔ 𝐶 = ∪ 𝑦 )
77 73 76 anbi12i ⊢ ( ( 𝑥 Bigcup 𝑦 ∧ 𝑦 Bigcup 𝐶 ) ↔ ( 𝑦 = ∪ 𝑥 ∧ 𝐶 = ∪ 𝑦 ) )
78 77 exbii ⊢ ( ∃ 𝑦 ( 𝑥 Bigcup 𝑦 ∧ 𝑦 Bigcup 𝐶 ) ↔ ∃ 𝑦 ( 𝑦 = ∪ 𝑥 ∧ 𝐶 = ∪ 𝑦 ) )
79 vuniex ⊢ ∪ 𝑥 ∈ V
80 unieq ⊢ ( 𝑦 = ∪ 𝑥 → ∪ 𝑦 = ∪ ∪ 𝑥 )
81 80 eqeq2d ⊢ ( 𝑦 = ∪ 𝑥 → ( 𝐶 = ∪ 𝑦 ↔ 𝐶 = ∪ ∪ 𝑥 ) )
82 79 81 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = ∪ 𝑥 ∧ 𝐶 = ∪ 𝑦 ) ↔ 𝐶 = ∪ ∪ 𝑥 )
83 70 78 82 3bitri ⊢ ( 𝑥 ( Bigcup ∘ Bigcup ) 𝐶 ↔ 𝐶 = ∪ ∪ 𝑥 )
84 69 83 anbi12i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) 𝑥 ∧ 𝑥 ( Bigcup ∘ Bigcup ) 𝐶 ) ↔ ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ∧ 𝐶 = ∪ ∪ 𝑥 ) )
85 84 exbii ⊢ ( ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ↾ Singletons ) ⊗ V ) ) ) ∘ ( ( Singleton ∘ Img ) ∘ pprod ( I , Singleton ) ) ) 𝑥 ∧ 𝑥 ( Bigcup ∘ Bigcup ) 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ∧ 𝐶 = ∪ ∪ 𝑥 ) )
86 11 13 85 3bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Apply 𝐶 ↔ ∃ 𝑥 ( 𝑥 = ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) ∧ 𝐶 = ∪ ∪ 𝑥 ) )
87 dffv5 ⊢ ( 𝐴 ‘ 𝐵 ) = ∪ ∪ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons )
88 87 eqeq2i ⊢ ( 𝐶 = ( 𝐴 ‘ 𝐵 ) ↔ 𝐶 = ∪ ∪ ( { ( 𝐴 “ { 𝐵 } ) } ∩ Singletons ) )
89 9 86 88 3bitr4i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Apply 𝐶 ↔ 𝐶 = ( 𝐴 ‘ 𝐵 ) )