Metamath Proof Explorer

Theorem fununi

Description: The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004)

Ref Expression
Assertion fununi ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ∪ 𝐴 )

Proof

Step Hyp Ref Expression
1 funrel ⊢ ( Fun 𝑓 → Rel 𝑓 )
2 1 adantr ⊢ ( ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Rel 𝑓 )
3 2 ralimi ⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑓 ∈ 𝐴 Rel 𝑓 )
4 reluni ⊢ ( Rel ∪ 𝐴 ↔ ∀ 𝑓 ∈ 𝐴 Rel 𝑓 )
5 3 4 sylibr ⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Rel ∪ 𝐴 )
6 r19.28v ⊢ ( ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) )
7 6 ralimi ⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) )
8 ssel ⊢ ( 𝑤 ⊆ 𝑣 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑣 ) )
9 8 anim1d ⊢ ( 𝑤 ⊆ 𝑣 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑣 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) )
10 dffun4 ⊢ ( Fun 𝑣 ↔ ( Rel 𝑣 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑣 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
11 10 simprbi ⊢ ( Fun 𝑣 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑣 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
12 11 19.21bbi ⊢ ( Fun 𝑣 → ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑣 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
13 12 19.21bi ⊢ ( Fun 𝑣 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑣 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
14 9 13 syl9r ⊢ ( Fun 𝑣 → ( 𝑤 ⊆ 𝑣 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
15 14 adantl ⊢ ( ( Fun 𝑤 ∧ Fun 𝑣 ) → ( 𝑤 ⊆ 𝑣 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
16 ssel ⊢ ( 𝑣 ⊆ 𝑤 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑤 ) )
17 16 anim2d ⊢ ( 𝑣 ⊆ 𝑤 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑤 ) ) )
18 dffun4 ⊢ ( Fun 𝑤 ↔ ( Rel 𝑤 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑤 ) → 𝑦 = 𝑧 ) ) )
19 18 simprbi ⊢ ( Fun 𝑤 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑤 ) → 𝑦 = 𝑧 ) )
20 19 19.21bbi ⊢ ( Fun 𝑤 → ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑤 ) → 𝑦 = 𝑧 ) )
21 20 19.21bi ⊢ ( Fun 𝑤 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑤 ) → 𝑦 = 𝑧 ) )
22 17 21 syl9r ⊢ ( Fun 𝑤 → ( 𝑣 ⊆ 𝑤 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
23 22 adantr ⊢ ( ( Fun 𝑤 ∧ Fun 𝑣 ) → ( 𝑣 ⊆ 𝑤 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
24 15 23 jaod ⊢ ( ( Fun 𝑤 ∧ Fun 𝑣 ) → ( ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
25 24 imp ⊢ ( ( ( Fun 𝑤 ∧ Fun 𝑣 ) ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
26 25 2ralimi ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( Fun 𝑤 ∧ Fun 𝑣 ) ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
27 funeq ⊢ ( 𝑓 = 𝑤 → ( Fun 𝑓 ↔ Fun 𝑤 ) )
28 sseq1 ⊢ ( 𝑓 = 𝑤 → ( 𝑓 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑔 ) )
29 sseq2 ⊢ ( 𝑓 = 𝑤 → ( 𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑤 ) )
30 28 29 orbi12d ⊢ ( 𝑓 = 𝑤 → ( ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ↔ ( 𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤 ) ) )
31 27 30 anbi12d ⊢ ( 𝑓 = 𝑤 → ( ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤 ) ) ) )
32 sseq2 ⊢ ( 𝑔 = 𝑣 → ( 𝑤 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑣 ) )
33 sseq1 ⊢ ( 𝑔 = 𝑣 → ( 𝑔 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤 ) )
34 32 33 orbi12d ⊢ ( 𝑔 = 𝑣 → ( ( 𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤 ) ↔ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
35 34 anbi2d ⊢ ( 𝑔 = 𝑣 → ( ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤 ) ) ↔ ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) )
36 31 35 cbvral2vw ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
37 ralcom ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ∀ 𝑔 ∈ 𝐴 ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) )
38 orcom ⊢ ( ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ↔ ( 𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔 ) )
39 sseq1 ⊢ ( 𝑔 = 𝑤 → ( 𝑔 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑓 ) )
40 sseq2 ⊢ ( 𝑔 = 𝑤 → ( 𝑓 ⊆ 𝑔 ↔ 𝑓 ⊆ 𝑤 ) )
41 39 40 orbi12d ⊢ ( 𝑔 = 𝑤 → ( ( 𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔 ) ↔ ( 𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤 ) ) )
42 38 41 bitrid ⊢ ( 𝑔 = 𝑤 → ( ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ↔ ( 𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤 ) ) )
43 42 anbi2d ⊢ ( 𝑔 = 𝑤 → ( ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ( Fun 𝑓 ∧ ( 𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤 ) ) ) )
44 funeq ⊢ ( 𝑓 = 𝑣 → ( Fun 𝑓 ↔ Fun 𝑣 ) )
45 sseq2 ⊢ ( 𝑓 = 𝑣 → ( 𝑤 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑣 ) )
46 sseq1 ⊢ ( 𝑓 = 𝑣 → ( 𝑓 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤 ) )
47 45 46 orbi12d ⊢ ( 𝑓 = 𝑣 → ( ( 𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤 ) ↔ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
48 44 47 anbi12d ⊢ ( 𝑓 = 𝑣 → ( ( Fun 𝑓 ∧ ( 𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤 ) ) ↔ ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) )
49 43 48 cbvral2vw ⊢ ( ∀ 𝑔 ∈ 𝐴 ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
50 37 49 bitri ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
51 36 50 anbi12i ⊢ ( ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ) ↔ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) )
52 anidm ⊢ ( ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) )
53 anandir ⊢ ( ( ( Fun 𝑤 ∧ Fun 𝑣 ) ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ↔ ( ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ∧ ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) )
54 53 2ralbii ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( Fun 𝑤 ∧ Fun 𝑣 ) ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ∧ ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) )
55 r19.26-2 ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ∧ ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) ↔ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) )
56 54 55 bitr2i ⊢ ( ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑤 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( Fun 𝑣 ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( Fun 𝑤 ∧ Fun 𝑣 ) ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
57 51 52 56 3bitr3i ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( Fun 𝑤 ∧ Fun 𝑣 ) ∧ ( 𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤 ) ) )
58 eluni ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) )
59 eluni ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) )
60 58 59 anbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) ↔ ( ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ∧ ∃ 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) ) )
61 exdistrv ⊢ ( ∃ 𝑤 ∃ 𝑣 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) ) ↔ ( ∃ 𝑤 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ∧ ∃ 𝑣 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) ) )
62 an4 ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) )
63 62 biancomi ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) )
64 63 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑣 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) ) ↔ ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) )
65 60 61 64 3bitr2i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) ↔ ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) )
66 65 imbi1i ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) )
67 19.23v ⊢ ( ∀ 𝑤 ( ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) )
68 r2al ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
69 impexp ⊢ ( ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
70 69 2albii ⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) ) )
71 19.23v ⊢ ( ∀ 𝑣 ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) )
72 71 albii ⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑤 ( ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) )
73 68 70 72 3bitr2ri ⊢ ( ∀ 𝑤 ( ∃ 𝑣 ( ( 𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
74 66 67 73 3bitr2i ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑣 ) → 𝑦 = 𝑧 ) )
75 26 57 74 3imtr4i ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) )
76 75 alrimiv ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) )
77 76 alrimivv ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( Fun 𝑓 ∧ ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) )
78 7 77 syl ⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) )
79 dffun4 ⊢ ( Fun ∪ 𝐴 ↔ ( Rel ∪ 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝐴 ) → 𝑦 = 𝑧 ) ) )
80 5 78 79 sylanbrc ⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ∪ 𝐴 )