This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )