Metamath Proof Explorer

Theorem ptpjpre1

Description: The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015)

Ref Expression
Hypothesis ptpjpre1.1 ⊢ 𝑋 = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 )
Assertion ptpjpre1 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 ptpjpre1.1 ⊢ 𝑋 = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 )
2 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝐼 ) )
3 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝐼 ) )
4 3 unieqd ⊢ ( 𝑘 = 𝐼 → ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝐼 ) )
5 2 4 eleq12d ⊢ ( 𝑘 = 𝐼 → ( ( 𝑤 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑤 ‘ 𝐼 ) ∈ ∪ ( 𝐹 ‘ 𝐼 ) ) )
6 vex ⊢ 𝑤 ∈ V
7 6 elixp ⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑤 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
8 7 simprbi ⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
9 8 1 eleq2s ⊢ ( 𝑤 ∈ 𝑋 → ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
10 9 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑤 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
11 simplrl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝐼 ∈ 𝐴 )
12 5 10 11 rspcdva ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ‘ 𝐼 ) ∈ ∪ ( 𝐹 ‘ 𝐼 ) )
13 12 fmpttd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝐼 ) )
14 ffn ⊢ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝐼 ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) Fn 𝑋 )
15 elpreima ⊢ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) Fn 𝑋 → ( 𝑧 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) ∈ 𝑈 ) ) )
16 13 14 15 3syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝑧 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) ∈ 𝑈 ) ) )
17 fveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ‘ 𝐼 ) = ( 𝑧 ‘ 𝐼 ) )
18 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) )
19 fvex ⊢ ( 𝑧 ‘ 𝐼 ) ∈ V
20 17 18 19 fvmpt ⊢ ( 𝑧 ∈ 𝑋 → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) = ( 𝑧 ‘ 𝐼 ) )
21 20 eleq1d ⊢ ( 𝑧 ∈ 𝑋 → ( ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) ∈ 𝑈 ↔ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) )
22 21 pm5.32i ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) ∈ 𝑈 ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) )
23 1 eleq2i ⊢ ( 𝑧 ∈ 𝑋 ↔ 𝑧 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
24 vex ⊢ 𝑧 ∈ V
25 24 elixp ⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
26 23 25 bitri ⊢ ( 𝑧 ∈ 𝑋 ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
27 26 anbi1i ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ↔ ( ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) )
28 anass ⊢ ( ( ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ↔ ( 𝑧 Fn 𝐴 ∧ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ) )
29 27 28 bitri ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ↔ ( 𝑧 Fn 𝐴 ∧ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ) )
30 22 29 bitri ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) ∈ 𝑈 ) ↔ ( 𝑧 Fn 𝐴 ∧ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ) )
31 simprl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ∧ ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 )
32 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑧 ‘ 𝑘 ) = ( 𝑧 ‘ 𝐼 ) )
33 iftrue ⊢ ( 𝑘 = 𝐼 → if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) = 𝑈 )
34 32 33 eleq12d ⊢ ( 𝑘 = 𝐼 → ( ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) )
35 31 34 syl5ibrcom ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ∧ ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑘 = 𝐼 → ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
36 simprr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ∧ ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
37 iffalse ⊢ ( ¬ 𝑘 = 𝐼 → if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) )
38 37 eleq2d ⊢ ( ¬ 𝑘 = 𝐼 → ( ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
39 36 38 syl5ibrcom ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ∧ ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) → ( ¬ 𝑘 = 𝐼 → ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
40 35 39 pm2.61d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ∧ ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) )
41 40 expr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) → ( ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) → ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
42 41 ralimdv ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
43 42 expimpd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ( ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
44 43 ancomsd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
45 elssuni ⊢ ( 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) → 𝑈 ⊆ ∪ ( 𝐹 ‘ 𝐼 ) )
46 45 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → 𝑈 ⊆ ∪ ( 𝐹 ‘ 𝐼 ) )
47 33 4 sseq12d ⊢ ( 𝑘 = 𝐼 → ( if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ↔ 𝑈 ⊆ ∪ ( 𝐹 ‘ 𝐼 ) ) )
48 46 47 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝑘 = 𝐼 → if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) )
49 ssid ⊢ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ( 𝐹 ‘ 𝑘 )
50 37 49 eqsstrdi ⊢ ( ¬ 𝑘 = 𝐼 → if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
51 48 50 pm2.61d1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
52 51 sseld ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
53 52 ralimdv ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
54 34 rspcv ⊢ ( 𝐼 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) )
55 54 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) )
56 53 55 jcad ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ) )
57 44 56 impbid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
58 57 anbi2d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ( 𝑧 Fn 𝐴 ∧ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑧 ‘ 𝐼 ) ∈ 𝑈 ) ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ) )
59 30 58 bitrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ( 𝑧 ∈ 𝑋 ∧ ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) ‘ 𝑧 ) ∈ 𝑈 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ) )
60 16 59 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝑧 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ) )
61 24 elixp ⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
62 60 61 bitr4di ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝑧 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) ↔ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
63 62 eqrdv ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼 ∈ 𝐴 ∧ 𝑈 ∈ ( 𝐹 ‘ 𝐼 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝐼 ) ) “ 𝑈 ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝐼 , 𝑈 , ∪ ( 𝐹 ‘ 𝑘 ) ) )