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

Metamath Proof Explorer

Theorem fpwwe2lem10

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
fpwwe2.4 ⊢ 𝑋 = ∪ dom 𝑊
Assertion fpwwe2lem10 ( 𝜑 → 𝑊 : dom 𝑊 ⟶ 𝒫 ( 𝑋 × 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2.4 ⊢ 𝑋 = ∪ dom 𝑊
5 1 relopabiv ⊢ Rel 𝑊
6 5 a1i ⊢ ( 𝜑 → Rel 𝑊 )
7 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑠 = ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) ) ) → 𝑠 = ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) )
8 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑤 𝑊 𝑡 ↔ ( ( 𝑤 ⊆ 𝐴 ∧ 𝑡 ⊆ ( 𝑤 × 𝑤 ) ) ∧ ( 𝑡 We 𝑤 ∧ ∀ 𝑦 ∈ 𝑤 [ ( ◡ 𝑡 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑡 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
9 8 simprbda ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑡 ) → ( 𝑤 ⊆ 𝐴 ∧ 𝑡 ⊆ ( 𝑤 × 𝑤 ) ) )
10 9 simprd ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑡 ) → 𝑡 ⊆ ( 𝑤 × 𝑤 ) )
11 10 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → 𝑡 ⊆ ( 𝑤 × 𝑤 ) )
12 11 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑠 = ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) ) ) → 𝑡 ⊆ ( 𝑤 × 𝑤 ) )
13 dfss2 ⊢ ( 𝑡 ⊆ ( 𝑤 × 𝑤 ) ↔ ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) = 𝑡 )
14 12 13 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑠 = ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) ) ) → ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) = 𝑡 )
15 7 14 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑠 = ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) ) ) → 𝑠 = 𝑡 )
16 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑡 = ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) ) ) → 𝑡 = ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) )
17 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑤 𝑊 𝑠 ↔ ( ( 𝑤 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑤 × 𝑤 ) ) ∧ ( 𝑠 We 𝑤 ∧ ∀ 𝑦 ∈ 𝑤 [ ( ◡ 𝑠 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑠 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
18 17 simprbda ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → ( 𝑤 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑤 × 𝑤 ) ) )
19 18 simprd ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → 𝑠 ⊆ ( 𝑤 × 𝑤 ) )
20 19 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → 𝑠 ⊆ ( 𝑤 × 𝑤 ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑡 = ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) ) ) → 𝑠 ⊆ ( 𝑤 × 𝑤 ) )
22 dfss2 ⊢ ( 𝑠 ⊆ ( 𝑤 × 𝑤 ) ↔ ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) = 𝑠 )
23 21 22 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑡 = ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) ) ) → ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) = 𝑠 )
24 16 23 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑤 ⊆ 𝑤 ∧ 𝑡 = ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) ) ) → 𝑠 = 𝑡 )
25 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → 𝐴 ∈ 𝑉 )
26 3 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
27 simprl ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → 𝑤 𝑊 𝑠 )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → 𝑤 𝑊 𝑡 )
29 1 25 26 27 28 fpwwe2lem9 ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → ( ( 𝑤 ⊆ 𝑤 ∧ 𝑠 = ( 𝑡 ∩ ( 𝑤 × 𝑤 ) ) ) ∨ ( 𝑤 ⊆ 𝑤 ∧ 𝑡 = ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) ) ) )
30 15 24 29 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) ) → 𝑠 = 𝑡 )
31 30 ex ⊢ ( 𝜑 → ( ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) → 𝑠 = 𝑡 ) )
32 31 alrimiv ⊢ ( 𝜑 → ∀ 𝑡 ( ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) → 𝑠 = 𝑡 ) )
33 32 alrimivv ⊢ ( 𝜑 → ∀ 𝑤 ∀ 𝑠 ∀ 𝑡 ( ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) → 𝑠 = 𝑡 ) )
34 dffun2 ⊢ ( Fun 𝑊 ↔ ( Rel 𝑊 ∧ ∀ 𝑤 ∀ 𝑠 ∀ 𝑡 ( ( 𝑤 𝑊 𝑠 ∧ 𝑤 𝑊 𝑡 ) → 𝑠 = 𝑡 ) ) )
35 6 33 34 sylanbrc ⊢ ( 𝜑 → Fun 𝑊 )
36 35 funfnd ⊢ ( 𝜑 → 𝑊 Fn dom 𝑊 )
37 vex ⊢ 𝑠 ∈ V
38 37 elrn ⊢ ( 𝑠 ∈ ran 𝑊 ↔ ∃ 𝑤 𝑤 𝑊 𝑠 )
39 5 releldmi ⊢ ( 𝑤 𝑊 𝑠 → 𝑤 ∈ dom 𝑊 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → 𝑤 ∈ dom 𝑊 )
41 elssuni ⊢ ( 𝑤 ∈ dom 𝑊 → 𝑤 ⊆ ∪ dom 𝑊 )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → 𝑤 ⊆ ∪ dom 𝑊 )
43 42 4 sseqtrrdi ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → 𝑤 ⊆ 𝑋 )
44 xpss12 ⊢ ( ( 𝑤 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( 𝑤 × 𝑤 ) ⊆ ( 𝑋 × 𝑋 ) )
45 43 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → ( 𝑤 × 𝑤 ) ⊆ ( 𝑋 × 𝑋 ) )
46 19 45 sstrd ⊢ ( ( 𝜑 ∧ 𝑤 𝑊 𝑠 ) → 𝑠 ⊆ ( 𝑋 × 𝑋 ) )
47 46 ex ⊢ ( 𝜑 → ( 𝑤 𝑊 𝑠 → 𝑠 ⊆ ( 𝑋 × 𝑋 ) ) )
48 velpw ⊢ ( 𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ↔ 𝑠 ⊆ ( 𝑋 × 𝑋 ) )
49 47 48 imbitrrdi ⊢ ( 𝜑 → ( 𝑤 𝑊 𝑠 → 𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) )
50 49 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑤 𝑤 𝑊 𝑠 → 𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) )
51 38 50 biimtrid ⊢ ( 𝜑 → ( 𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) )
52 51 ssrdv ⊢ ( 𝜑 → ran 𝑊 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
53 df-f ⊢ ( 𝑊 : dom 𝑊 ⟶ 𝒫 ( 𝑋 × 𝑋 ) ↔ ( 𝑊 Fn dom 𝑊 ∧ ran 𝑊 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ) )
54 36 52 53 sylanbrc ⊢ ( 𝜑 → 𝑊 : dom 𝑊 ⟶ 𝒫 ( 𝑋 × 𝑋 ) )