Metamath Proof Explorer


Theorem dffv2

Description: Alternate definition of function value df-fv that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010)

Ref Expression
Assertion dffv2 ( 𝐹𝐴 ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )

Proof

Step Hyp Ref Expression
1 snidb ( 𝐴 ∈ V ↔ 𝐴 ∈ { 𝐴 } )
2 fvres ( 𝐴 ∈ { 𝐴 } → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐹𝐴 ) )
3 1 2 sylbi ( 𝐴 ∈ V → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐹𝐴 ) )
4 fvprc ( ¬ 𝐴 ∈ V → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ∅ )
5 fvprc ( ¬ 𝐴 ∈ V → ( 𝐹𝐴 ) = ∅ )
6 4 5 eqtr4d ( ¬ 𝐴 ∈ V → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐹𝐴 ) )
7 3 6 pm2.61i ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐹𝐴 )
8 funfv ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) )
9 resima ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) = ( 𝐹 “ { 𝐴 } )
10 dif0 ( ( 𝐹 “ { 𝐴 } ) ∖ ∅ ) = ( 𝐹 “ { 𝐴 } )
11 9 10 eqtr4i ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ∅ )
12 df-fun ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ⊆ I ) )
13 12 simprbi ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ⊆ I )
14 ssdif0 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ⊆ I ↔ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) = ∅ )
15 13 14 sylib ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) = ∅ )
16 15 unieqd ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) = ∅ )
17 uni0 ∅ = ∅
18 16 17 eqtrdi ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) = ∅ )
19 18 unieqd ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) = ∅ )
20 19 17 eqtrdi ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) = ∅ )
21 20 difeq2d ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ∅ ) )
22 11 21 eqtr4id ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
23 22 unieqd ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
24 8 23 eqtrd ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
25 7 24 eqtr3id ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹𝐴 ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
26 nfunsn ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹𝐴 ) = ∅ )
27 relres Rel ( 𝐹 ↾ { 𝐴 } )
28 dffun3 ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ∀ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ) )
29 27 28 mpbiran ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ∀ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) )
30 iman ( ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ↔ ¬ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
31 30 albii ( ∀ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑧 ¬ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
32 alnex ( ∀ 𝑧 ¬ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ↔ ¬ ∃ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
33 31 32 bitri ( ∀ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ↔ ¬ ∃ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
34 33 exbii ( ∃ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ↔ ∃ 𝑦 ¬ ∃ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
35 exnal ( ∃ 𝑦 ¬ ∃ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ↔ ¬ ∀ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
36 34 35 bitri ( ∃ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ↔ ¬ ∀ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
37 36 albii ( ∀ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑥 ¬ ∀ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
38 alnex ( ∀ 𝑥 ¬ ∀ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ↔ ¬ ∃ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
39 29 37 38 3bitrri ( ¬ ∃ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ↔ Fun ( 𝐹 ↾ { 𝐴 } ) )
40 39 con1bii ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ∃ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
41 sp ( ∀ 𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ∃ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
42 41 eximi ( ∃ 𝑥𝑦𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ∃ 𝑥𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
43 40 42 sylbi ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ∃ 𝑥𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
44 snssi ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → { 𝐴 } ⊆ dom ( 𝐹 ↾ { 𝐴 } ) )
45 residm ( ( 𝐹 ↾ { 𝐴 } ) ↾ { 𝐴 } ) = ( 𝐹 ↾ { 𝐴 } )
46 45 dmeqi dom ( ( 𝐹 ↾ { 𝐴 } ) ↾ { 𝐴 } ) = dom ( 𝐹 ↾ { 𝐴 } )
47 ssdmres ( { 𝐴 } ⊆ dom ( 𝐹 ↾ { 𝐴 } ) ↔ dom ( ( 𝐹 ↾ { 𝐴 } ) ↾ { 𝐴 } ) = { 𝐴 } )
48 47 biimpi ( { 𝐴 } ⊆ dom ( 𝐹 ↾ { 𝐴 } ) → dom ( ( 𝐹 ↾ { 𝐴 } ) ↾ { 𝐴 } ) = { 𝐴 } )
49 46 48 eqtr3id ( { 𝐴 } ⊆ dom ( 𝐹 ↾ { 𝐴 } ) → dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } )
50 44 49 syl ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } )
51 vex 𝑥 ∈ V
52 vex 𝑧 ∈ V
53 51 52 breldm ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) )
54 eleq2 ( dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } → ( 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ↔ 𝑥 ∈ { 𝐴 } ) )
55 velsn ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
56 54 55 bitrdi ( dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } → ( 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ↔ 𝑥 = 𝐴 ) )
57 56 biimpa ( ( dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } ∧ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ) → 𝑥 = 𝐴 )
58 50 53 57 syl2an ( ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∧ 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) → 𝑥 = 𝐴 )
59 58 breq1d ( ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∧ 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
60 59 biimpd ( ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∧ 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
61 60 ex ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ) )
62 61 pm2.43d ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
63 62 anim1d ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ) )
64 63 eximdv ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ∃ 𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ∃ 𝑧 ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ) )
65 64 exlimdv ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ∃ 𝑥𝑧 ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ∃ 𝑧 ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ) )
66 43 65 mpan9 ( ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ) → ∃ 𝑧 ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) )
67 9 eleq2i ( 𝑦 ∈ ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) ↔ 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) )
68 elimasni ( 𝑦 ∈ ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) → 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
69 67 68 sylbir ( 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) → 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
70 vex 𝑦 ∈ V
71 70 52 uniop 𝑦 , 𝑧 ⟩ = { 𝑦 , 𝑧 }
72 opex 𝑦 , 𝑧 ⟩ ∈ V
73 72 unisn { ⟨ 𝑦 , 𝑧 ⟩ } = ⟨ 𝑦 , 𝑧
74 27 brrelex1i ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ∈ V )
75 brcnvg ( ( 𝑦 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
76 70 74 75 sylancr ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 → ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
77 76 biimpar ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴 )
78 74 adantl ( ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) → 𝐴 ∈ V )
79 breq2 ( 𝑥 = 𝐴 → ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴 ) )
80 breq1 ( 𝑥 = 𝐴 → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
81 79 80 anbi12d ( 𝑥 = 𝐴 → ( ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ↔ ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ) )
82 81 rspcev ( ( 𝐴 ∈ V ∧ ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ) → ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
83 78 82 mpancom ( ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) → ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
84 83 ancoms ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝐴 ) → ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
85 77 84 syldan ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
86 85 anim1i ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) ∧ ¬ 𝑧 = 𝑦 ) → ( ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ∧ ¬ 𝑧 = 𝑦 ) )
87 86 an32s ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → ( ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ∧ ¬ 𝑧 = 𝑦 ) )
88 eldif ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ↔ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∧ ¬ ⟨ 𝑦 , 𝑧 ⟩ ∈ I ) )
89 rexv ( ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ↔ ∃ 𝑥 ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
90 70 52 brco ( 𝑦 ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) 𝑧 ↔ ∃ 𝑥 ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
91 df-br ( 𝑦 ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) )
92 89 90 91 3bitr2ri ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ↔ ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) )
93 52 ideq ( 𝑦 I 𝑧𝑦 = 𝑧 )
94 df-br ( 𝑦 I 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ I )
95 equcom ( 𝑦 = 𝑧𝑧 = 𝑦 )
96 93 94 95 3bitr3i ( ⟨ 𝑦 , 𝑧 ⟩ ∈ I ↔ 𝑧 = 𝑦 )
97 96 notbii ( ¬ ⟨ 𝑦 , 𝑧 ⟩ ∈ I ↔ ¬ 𝑧 = 𝑦 )
98 92 97 anbi12i ( ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∧ ¬ ⟨ 𝑦 , 𝑧 ⟩ ∈ I ) ↔ ( ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ∧ ¬ 𝑧 = 𝑦 ) )
99 88 98 bitr2i ( ( ∃ 𝑥 ∈ V ( 𝑦 ( 𝐹 ↾ { 𝐴 } ) 𝑥𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ) ∧ ¬ 𝑧 = 𝑦 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
100 87 99 sylib ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
101 snssi ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) → { ⟨ 𝑦 , 𝑧 ⟩ } ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
102 uniss ( { ⟨ 𝑦 , 𝑧 ⟩ } ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) → { ⟨ 𝑦 , 𝑧 ⟩ } ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
103 100 101 102 3syl ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → { ⟨ 𝑦 , 𝑧 ⟩ } ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
104 73 103 eqsstrrid ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → ⟨ 𝑦 , 𝑧 ⟩ ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
105 104 unissd ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → 𝑦 , 𝑧 ⟩ ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
106 71 105 eqsstrrid ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → { 𝑦 , 𝑧 } ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
107 70 52 prss ( ( 𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ∧ 𝑧 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) ↔ { 𝑦 , 𝑧 } ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
108 106 107 sylibr ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → ( 𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ∧ 𝑧 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
109 108 simpld ( ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) ∧ 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) → 𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
110 109 ex ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑦𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
111 69 110 syl5 ( ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ( 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) → 𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
112 111 exlimiv ( ∃ 𝑧 ( 𝐴 ( 𝐹 ↾ { 𝐴 } ) 𝑧 ∧ ¬ 𝑧 = 𝑦 ) → ( 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) → 𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
113 66 112 syl ( ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝑦 ∈ ( 𝐹 “ { 𝐴 } ) → 𝑦 ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
114 113 ssrdv ( ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 “ { 𝐴 } ) ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )
115 ssdif0 ( ( 𝐹 “ { 𝐴 } ) ⊆ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ↔ ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ )
116 114 115 sylib ( ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ )
117 116 ex ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ ) )
118 ndmima ( ¬ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 ↾ { 𝐴 } ) “ { 𝐴 } ) = ∅ )
119 9 118 eqtr3id ( ¬ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 “ { 𝐴 } ) = ∅ )
120 119 difeq1d ( ¬ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ( ∅ ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
121 0dif ( ∅ ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅
122 120 121 eqtrdi ( ¬ 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ )
123 117 122 pm2.61d1 ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ )
124 123 unieqd ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ )
125 124 17 eqtrdi ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) = ∅ )
126 26 125 eqtr4d ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹𝐴 ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) ) )
127 25 126 pm2.61i ( 𝐹𝐴 ) = ( ( 𝐹 “ { 𝐴 } ) ∖ ( ( ( 𝐹 ↾ { 𝐴 } ) ∘ ( 𝐹 ↾ { 𝐴 } ) ) ∖ I ) )