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

Metamath Proof Explorer

Theorem fncnv

Description: Single-rootedness (see funcnv ) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007)

Ref Expression
Assertion fncnv ( ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) Fn 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )

Proof

Step Hyp Ref Expression
1 df-fn ⊢ ( ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) Fn 𝐵 ↔ ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
2 df-rn ⊢ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) )
3 2 eqeq1i ⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 )
4 3 anbi2i ⊢ ( ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) ↔ ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
5 rninxp ⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )
6 5 anbi1i ⊢ ( ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
7 funcnv ⊢ ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑦 ∈ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 )
8 raleq ⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 → ( ∀ 𝑦 ∈ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
9 moanimv ⊢ ( ∃* 𝑥 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
10 brinxp2 ⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
11 an21 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
12 10 11 bitri ⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
13 12 mobii ⊢ ( ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∃* 𝑥 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
14 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
15 14 imbi2i ⊢ ( ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
16 9 13 15 3bitr4i ⊢ ( ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
17 biimt ⊢ ( 𝑦 ∈ 𝐵 → ( ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ) )
18 16 17 bitr4id ⊢ ( 𝑦 ∈ 𝐵 → ( ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
19 18 ralbiia ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )
20 8 19 bitrdi ⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 → ( ∀ 𝑦 ∈ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
21 7 20 bitrid ⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 → ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
22 21 pm5.32i ⊢ ( ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) ↔ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
23 r19.26 ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
24 6 22 23 3bitr4i ⊢ ( ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
25 ancom ⊢ ( ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) ↔ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
26 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
27 26 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
28 24 25 27 3bitr4i ⊢ ( ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )
29 1 4 28 3bitr2i ⊢ ( ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) Fn 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )