Metamath Proof Explorer

Theorem firest

Description: The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion firest ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) = ( ( fi ‘ 𝐽 ) ↾t 𝐴 )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝐽 ↾t 𝐴 ) ∈ V
2 elfi2 ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ V → ( 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) 𝑥 = ∩ 𝑦 ) )
3 1 2 ax-mp ⊢ ( 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) 𝑥 = ∩ 𝑦 )
4 eldifi ⊢ ( 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) → 𝑦 ∈ ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) )
5 4 adantl ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ∈ ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) )
6 5 elin2d ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ∈ Fin )
7 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ↔ ( 𝑦 ⊆ ( 𝐽 ↾t 𝐴 ) ∧ 𝑦 ∈ Fin ) )
8 7 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) → 𝑦 ⊆ ( 𝐽 ↾t 𝐴 ) )
9 5 8 syl ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ⊆ ( 𝐽 ↾t 𝐴 ) )
10 9 sseld ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ) )
11 elrest ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ 𝐴 ) ) )
12 11 adantr ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ 𝐴 ) ) )
13 10 12 sylibd ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ 𝐴 ) ) )
14 13 ralrimiv ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ∀ 𝑧 ∈ 𝑦 ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ 𝐴 ) )
15 ineq1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( 𝑦 ∩ 𝐴 ) = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) )
16 15 eqeq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( 𝑧 = ( 𝑦 ∩ 𝐴 ) ↔ 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ) )
17 16 ac6sfi ⊢ ( ( 𝑦 ∈ Fin ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 : 𝑦 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ) )
18 6 14 17 syl2anc ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ∃ 𝑓 ( 𝑓 : 𝑦 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ) )
19 eldifsni ⊢ ( 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) → 𝑦 ≠ ∅ )
20 19 ad2antlr ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → 𝑦 ≠ ∅ )
21 iinin1 ⊢ ( 𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) = ( ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) )
22 20 21 syl ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ∩ 𝑧 ∈ 𝑦 ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) = ( ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) )
23 fvex ⊢ ( fi ‘ 𝐽 ) ∈ V
24 simpllr ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → 𝐴 ∈ V )
25 ffn ⊢ ( 𝑓 : 𝑦 ⟶ 𝐽 → 𝑓 Fn 𝑦 )
26 25 adantl ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → 𝑓 Fn 𝑦 )
27 fniinfv ⊢ ( 𝑓 Fn 𝑦 → ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) = ∩ ran 𝑓 )
28 26 27 syl ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) = ∩ ran 𝑓 )
29 simplll ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → 𝐽 ∈ V )
30 simpr ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → 𝑓 : 𝑦 ⟶ 𝐽 )
31 6 adantr ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → 𝑦 ∈ Fin )
32 intrnfi ⊢ ( ( 𝐽 ∈ V ∧ ( 𝑓 : 𝑦 ⟶ 𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin ) ) → ∩ ran 𝑓 ∈ ( fi ‘ 𝐽 ) )
33 29 30 20 31 32 syl13anc ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ∩ ran 𝑓 ∈ ( fi ‘ 𝐽 ) )
34 28 33 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) ∈ ( fi ‘ 𝐽 ) )
35 elrestr ⊢ ( ( ( fi ‘ 𝐽 ) ∈ V ∧ 𝐴 ∈ V ∧ ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) ∈ ( fi ‘ 𝐽 ) ) → ( ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) )
36 23 24 34 35 mp3an2i ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ( ∩ 𝑧 ∈ 𝑦 ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) )
37 22 36 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ∩ 𝑧 ∈ 𝑦 ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) )
38 intiin ⊢ ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 𝑧
39 iineq2 ⊢ ( ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) → ∩ 𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) )
40 38 39 eqtrid ⊢ ( ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) )
41 40 eleq1d ⊢ ( ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) → ( ∩ 𝑦 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ↔ ∩ 𝑧 ∈ 𝑦 ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
42 37 41 syl5ibrcom ⊢ ( ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) ∧ 𝑓 : 𝑦 ⟶ 𝐽 ) → ( ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) → ∩ 𝑦 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
43 42 expimpd ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ( ( 𝑓 : 𝑦 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ) → ∩ 𝑦 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
44 43 exlimdv ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑦 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑦 𝑧 = ( ( 𝑓 ‘ 𝑧 ) ∩ 𝐴 ) ) → ∩ 𝑦 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
45 18 44 mpd ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑦 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) )
46 eleq1 ⊢ ( 𝑥 = ∩ 𝑦 → ( 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ↔ ∩ 𝑦 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
47 45 46 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 = ∩ 𝑦 → 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
48 47 rexlimdva ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( ∃ 𝑦 ∈ ( ( 𝒫 ( 𝐽 ↾t 𝐴 ) ∩ Fin ) ∖ { ∅ } ) 𝑥 = ∩ 𝑦 → 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
49 3 48 syl5bi ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
50 simpr ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → 𝐴 ∈ V )
51 elrest ⊢ ( ( ( fi ‘ 𝐽 ) ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ ( fi ‘ 𝐽 ) 𝑥 = ( 𝑧 ∩ 𝐴 ) ) )
52 23 50 51 sylancr ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ ( fi ‘ 𝐽 ) 𝑥 = ( 𝑧 ∩ 𝐴 ) ) )
53 elfi2 ⊢ ( 𝐽 ∈ V → ( 𝑧 ∈ ( fi ‘ 𝐽 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 ) )
54 53 adantr ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( fi ‘ 𝐽 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 ) )
55 eldifsni ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ≠ ∅ )
56 55 adantl ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ≠ ∅ )
57 iinin1 ⊢ ( 𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) = ( ∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴 ) )
58 56 57 syl ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) = ( ∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴 ) )
59 38 ineq1i ⊢ ( ∩ 𝑦 ∩ 𝐴 ) = ( ∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴 )
60 58 59 eqtr4di ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) = ( ∩ 𝑦 ∩ 𝐴 ) )
61 ovexd ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝐽 ↾t 𝐴 ) ∈ V )
62 eldifi ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ∈ ( 𝒫 𝐽 ∩ Fin ) )
63 62 adantl ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ∈ ( 𝒫 𝐽 ∩ Fin ) )
64 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 𝐽 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin ) )
65 64 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐽 ∩ Fin ) → 𝑦 ⊆ 𝐽 )
66 63 65 syl ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ⊆ 𝐽 )
67 elrestr ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
68 67 3expa ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
69 68 ralrimiva ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ∀ 𝑧 ∈ 𝐽 ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
70 69 adantr ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ∀ 𝑧 ∈ 𝐽 ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
71 ssralv ⊢ ( 𝑦 ⊆ 𝐽 → ( ∀ 𝑧 ∈ 𝐽 ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ) )
72 66 70 71 sylc ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
73 63 elin2d ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ∈ Fin )
74 iinfi ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ V ∧ ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin ) ) → ∩ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) )
75 61 72 56 73 74 syl13anc ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝐴 ) ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) )
76 60 75 eqeltrrd ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ( ∩ 𝑦 ∩ 𝐴 ) ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) )
77 eleq1 ⊢ ( 𝑥 = ( ∩ 𝑦 ∩ 𝐴 ) → ( 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ( ∩ 𝑦 ∩ 𝐴 ) ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) )
78 76 77 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 = ( ∩ 𝑦 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) )
79 ineq1 ⊢ ( 𝑧 = ∩ 𝑦 → ( 𝑧 ∩ 𝐴 ) = ( ∩ 𝑦 ∩ 𝐴 ) )
80 79 eqeq2d ⊢ ( 𝑧 = ∩ 𝑦 → ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ↔ 𝑥 = ( ∩ 𝑦 ∩ 𝐴 ) ) )
81 80 imbi1d ⊢ ( 𝑧 = ∩ 𝑦 → ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) ↔ ( 𝑥 = ( ∩ 𝑦 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) ) )
82 78 81 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ∧ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑧 = ∩ 𝑦 → ( 𝑥 = ( 𝑧 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) ) )
83 82 rexlimdva ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( ∃ 𝑦 ∈ ( ( 𝒫 𝐽 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 → ( 𝑥 = ( 𝑧 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) ) )
84 54 83 sylbid ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( fi ‘ 𝐽 ) → ( 𝑥 = ( 𝑧 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) ) )
85 84 rexlimdv ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( ∃ 𝑧 ∈ ( fi ‘ 𝐽 ) 𝑥 = ( 𝑧 ∩ 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) )
86 52 85 sylbid ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) → 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ) )
87 49 86 impbid ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ 𝑥 ∈ ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) ) )
88 87 eqrdv ⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) = ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) )
89 fi0 ⊢ ( fi ‘ ∅ ) = ∅
90 relxp ⊢ Rel ( V × V )
91 restfn ⊢ ↾t Fn ( V × V )
92 91 fndmi ⊢ dom ↾t = ( V × V )
93 92 releqi ⊢ ( Rel dom ↾t ↔ Rel ( V × V ) )
94 90 93 mpbir ⊢ Rel dom ↾t
95 94 ovprc ⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ∅ )
96 95 fveq2d ⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) = ( fi ‘ ∅ ) )
97 ianor ⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) ↔ ( ¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V ) )
98 fvprc ⊢ ( ¬ 𝐽 ∈ V → ( fi ‘ 𝐽 ) = ∅ )
99 98 oveq1d ⊢ ( ¬ 𝐽 ∈ V → ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) = ( ∅ ↾t 𝐴 ) )
100 0rest ⊢ ( ∅ ↾t 𝐴 ) = ∅
101 99 100 eqtrdi ⊢ ( ¬ 𝐽 ∈ V → ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) = ∅ )
102 94 ovprc2 ⊢ ( ¬ 𝐴 ∈ V → ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) = ∅ )
103 101 102 jaoi ⊢ ( ( ¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V ) → ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) = ∅ )
104 97 103 sylbi ⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) = ∅ )
105 89 96 104 3eqtr4a ⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) = ( ( fi ‘ 𝐽 ) ↾t 𝐴 ) )
106 88 105 pm2.61i ⊢ ( fi ‘ ( 𝐽 ↾t 𝐴 ) ) = ( ( fi ‘ 𝐽 ) ↾t 𝐴 )