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 syl5bb ( 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 𝐵 ↔ ∀ 𝑦𝐵 ∃! 𝑥𝐴 𝑥 𝑅 𝑦 )