MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iundom2g Structured version   Visualization version   GIF version

Theorem iundom2g 9615
Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. 𝐵 depends on 𝑥 and should be thought of as 𝐵(𝑥). (Contributed by Mario Carneiro, 1-Sep-2015.)
Hypotheses
Ref Expression
iunfo.1 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
iundomg.2 (𝜑 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴)
iundomg.3 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
Assertion
Ref Expression
iundom2g (𝜑𝑇 ≼ (𝐴 × 𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑇(𝑥)

Proof of Theorem iundom2g
Dummy variables 𝑓 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iundomg.2 . . 3 (𝜑 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴)
2 iundomg.3 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 brdomi 8171 . . . . . . . . 9 (𝐵𝐶 → ∃𝑔 𝑔:𝐵1-1𝐶)
43adantl 473 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑔:𝐵1-1𝐶)
5 f1f 6283 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐶𝑔:𝐵𝐶)
6 reldom 8166 . . . . . . . . . . . . . . 15 Rel ≼
76brrelex2i 5329 . . . . . . . . . . . . . 14 (𝐵𝐶𝐶 ∈ V)
86brrelex1i 5328 . . . . . . . . . . . . . 14 (𝐵𝐶𝐵 ∈ V)
97, 8elmapd 8074 . . . . . . . . . . . . 13 (𝐵𝐶 → (𝑔 ∈ (𝐶𝑚 𝐵) ↔ 𝑔:𝐵𝐶))
109adantl 473 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶𝑚 𝐵) ↔ 𝑔:𝐵𝐶))
115, 10syl5ibr 237 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 ∈ (𝐶𝑚 𝐵)))
12 ssiun2 4719 . . . . . . . . . . . . 13 (𝑥𝐴 → (𝐶𝑚 𝐵) ⊆ 𝑥𝐴 (𝐶𝑚 𝐵))
1312adantr 472 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝐶𝑚 𝐵) ⊆ 𝑥𝐴 (𝐶𝑚 𝐵))
1413sseld 3760 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶𝑚 𝐵) → 𝑔 𝑥𝐴 (𝐶𝑚 𝐵)))
1511, 14syld 47 . . . . . . . . . 10 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 𝑥𝐴 (𝐶𝑚 𝐵)))
1615ancrd 547 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶 → (𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
1716eximdv 2012 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → (∃𝑔 𝑔:𝐵1-1𝐶 → ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
184, 17mpd 15 . . . . . . 7 ((𝑥𝐴𝐵𝐶) → ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶))
19 df-rex 3061 . . . . . . 7 (∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶))
2018, 19sylibr 225 . . . . . 6 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
2120ralimiaa 3098 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
222, 21syl 17 . . . 4 (𝜑 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
23 nfv 2009 . . . . 5 𝑦𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶
24 nfiu1 4706 . . . . . 6 𝑥 𝑥𝐴 (𝐶𝑚 𝐵)
25 nfcv 2907 . . . . . . 7 𝑥𝑔
26 nfcsb1v 3707 . . . . . . 7 𝑥𝑦 / 𝑥𝐵
27 nfcv 2907 . . . . . . 7 𝑥𝐶
2825, 26, 27nff1 6281 . . . . . 6 𝑥 𝑔:𝑦 / 𝑥𝐵1-1𝐶
2924, 28nfrex 3153 . . . . 5 𝑥𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶
30 csbeq1a 3700 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
31 f1eq2 6279 . . . . . . 7 (𝐵 = 𝑦 / 𝑥𝐵 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3230, 31syl 17 . . . . . 6 (𝑥 = 𝑦 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3332rexbidv 3199 . . . . 5 (𝑥 = 𝑦 → (∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3423, 29, 33cbvral 3315 . . . 4 (∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
3522, 34sylib 209 . . 3 (𝜑 → ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
36 f1eq1 6278 . . . 4 (𝑔 = (𝑓𝑦) → (𝑔:𝑦 / 𝑥𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
3736acni3 9121 . . 3 (( 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴 ∧ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶) → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
381, 35, 37syl2anc 579 . 2 (𝜑 → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
39 nfv 2009 . . . . . 6 𝑦(𝑓𝑥):𝐵1-1𝐶
40 nfcv 2907 . . . . . . 7 𝑥(𝑓𝑦)
4140, 26, 27nff1 6281 . . . . . 6 𝑥(𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶
42 fveq2 6375 . . . . . . . 8 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
43 f1eq1 6278 . . . . . . . 8 ((𝑓𝑥) = (𝑓𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
4442, 43syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
45 f1eq2 6279 . . . . . . . 8 (𝐵 = 𝑦 / 𝑥𝐵 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4630, 45syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4744, 46bitrd 270 . . . . . 6 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4839, 41, 47cbvral 3315 . . . . 5 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ↔ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶)
49 df-ne 2938 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
50 acnrcl 9116 . . . . . . . . . 10 ( 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴𝐴 ∈ V)
511, 50syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ V)
52 r19.2z 4219 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → ∃𝑥𝐴 𝐵𝐶)
537rexlimivw 3176 . . . . . . . . . . . 12 (∃𝑥𝐴 𝐵𝐶𝐶 ∈ V)
5452, 53syl 17 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → 𝐶 ∈ V)
5554expcom 402 . . . . . . . . . 10 (∀𝑥𝐴 𝐵𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
562, 55syl 17 . . . . . . . . 9 (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
57 xpexg 7158 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V)
5851, 56, 57syl6an 674 . . . . . . . 8 (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V))
5949, 58syl5bir 234 . . . . . . 7 (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V))
60 xpeq1 5291 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶))
61 0xp 5369 . . . . . . . . 9 (∅ × 𝐶) = ∅
62 0ex 4950 . . . . . . . . 9 ∅ ∈ V
6361, 62eqeltri 2840 . . . . . . . 8 (∅ × 𝐶) ∈ V
6460, 63syl6eqel 2852 . . . . . . 7 (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)
6559, 64pm2.61d2 173 . . . . . 6 (𝜑 → (𝐴 × 𝐶) ∈ V)
66 iunfo.1 . . . . . . . . . 10 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
6766eleq2i 2836 . . . . . . . . 9 (𝑦𝑇𝑦 𝑥𝐴 ({𝑥} × 𝐵))
68 eliun 4680 . . . . . . . . 9 (𝑦 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
6967, 68bitri 266 . . . . . . . 8 (𝑦𝑇 ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
70 r19.29 3219 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)))
71 xp1st 7398 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (1st𝑦) ∈ {𝑥})
7271ad2antll 720 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ {𝑥})
73 elsni 4351 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ {𝑥} → (1st𝑦) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) = 𝑥)
75 simpl 474 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥𝐴)
7674, 75eqeltrd 2844 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ 𝐴)
7774fveq2d 6379 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st𝑦)) = (𝑓𝑥))
7877fveq1d 6377 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓𝑥)‘(2nd𝑦)))
79 f1f 6283 . . . . . . . . . . . . . . 15 ((𝑓𝑥):𝐵1-1𝐶 → (𝑓𝑥):𝐵𝐶)
8079ad2antrl 719 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓𝑥):𝐵𝐶)
81 xp2nd 7399 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ 𝐵)
8281ad2antll 720 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ 𝐵)
8380, 82ffvelrnd 6550 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓𝑥)‘(2nd𝑦)) ∈ 𝐶)
8478, 83eqeltrd 2844 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶)
85 opelxpi 5314 . . . . . . . . . . . 12 (((1st𝑦) ∈ 𝐴 ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8676, 84, 85syl2anc 579 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8786rexlimiva 3175 . . . . . . . . . 10 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8870, 87syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8988ex 401 . . . . . . . 8 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
9069, 89syl5bi 233 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
91 fvex 6388 . . . . . . . . . 10 (1st𝑦) ∈ V
92 fvex 6388 . . . . . . . . . 10 ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ V
9391, 92opth 5100 . . . . . . . . 9 (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ ((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
94 simpr 477 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) = (1st𝑧))
9594fveq2d 6379 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)) = (𝑓‘(1st𝑧)))
9695fveq1d 6377 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ((𝑓‘(1st𝑦))‘(2nd𝑧)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)))
9796eqeq2d 2775 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
98 djussxp 5436 . . . . . . . . . . . . . . . . . 18 𝑥𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
9966, 98eqsstri 3795 . . . . . . . . . . . . . . . . 17 𝑇 ⊆ (𝐴 × V)
100 simprl 787 . . . . . . . . . . . . . . . . 17 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦𝑇)
10199, 100sseldi 3759 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦 ∈ (𝐴 × V))
102101adantr 472 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → 𝑦 ∈ (𝐴 × V))
103 xp1st 7398 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐴 × V) → (1st𝑦) ∈ 𝐴)
104102, 103syl 17 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) ∈ 𝐴)
105 simpll 783 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶)
106 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑥(𝑓‘(1st𝑦))
107 nfcsb1v 3707 . . . . . . . . . . . . . . . 16 𝑥(1st𝑦) / 𝑥𝐵
108106, 107, 27nff1 6281 . . . . . . . . . . . . . . 15 𝑥(𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶
109 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → (𝑓𝑥) = (𝑓‘(1st𝑦)))
110 f1eq1 6278 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) = (𝑓‘(1st𝑦)) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
111109, 110syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
112 csbeq1a 3700 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → 𝐵 = (1st𝑦) / 𝑥𝐵)
113 f1eq2 6279 . . . . . . . . . . . . . . . . 17 (𝐵 = (1st𝑦) / 𝑥𝐵 → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
115111, 114bitrd 270 . . . . . . . . . . . . . . 15 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
116108, 115rspc 3455 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ 𝐴 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
117104, 105, 116sylc 65 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶)
118107nfel2 2924 . . . . . . . . . . . . . . . . . . . 20 𝑥(2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵
11974eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st𝑦))
120119, 112syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = (1st𝑦) / 𝑥𝐵)
12182, 120eleqtrd 2846 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
122121ex 401 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴 → (((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
123118, 122rexlimi 3171 . . . . . . . . . . . . . . . . . . 19 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
12470, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
125124ex 401 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
12669, 125syl5bi 233 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
127126imp 395 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑦𝑇) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
128127adantrr 708 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
129128adantr 472 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
130126ralrimiv 3112 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
131 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (2nd𝑦) = (2nd𝑧))
132 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (1st𝑦) = (1st𝑧))
133132csbeq1d 3698 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧(1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
134131, 133eleq12d 2838 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ↔ (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵))
135134rspccva 3460 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
136130, 135sylan 575 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
137136adantrl 707 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
138137adantr 472 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
13994csbeq1d 3698 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
140138, 139eleqtrrd 2847 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)
141 f1fveq 6711 . . . . . . . . . . . . 13 (((𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶 ∧ ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ∧ (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
142117, 129, 140, 141syl12anc 865 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
14397, 142bitr3d 272 . . . . . . . . . . 11 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
144143pm5.32da 574 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ ((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧))))
145 simprr 789 . . . . . . . . . . . 12 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧𝑇)
14699, 145sseldi 3759 . . . . . . . . . . 11 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧 ∈ (𝐴 × V))
147 xpopth 7407 . . . . . . . . . . 11 ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
148101, 146, 147syl2anc 579 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
149144, 148bitrd 270 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ 𝑦 = 𝑧))
15093, 149syl5bb 274 . . . . . . . 8 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧))
151150ex 401 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝑦𝑇𝑧𝑇) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧)))
15290, 151dom2d 8201 . . . . . 6 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶)))
15365, 152syl5com 31 . . . . 5 (𝜑 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
15448, 153syl5bir 234 . . . 4 (𝜑 → (∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
155154adantld 484 . . 3 (𝜑 → ((𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
156155exlimdv 2028 . 2 (𝜑 → (∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
15738, 156mpd 15 1 (𝜑𝑇 ≼ (𝐴 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  csb 3691  wss 3732  c0 4079  {csn 4334  cop 4340   ciun 4676   class class class wbr 4809   × cxp 5275  wf 6064  1-1wf1 6065  cfv 6068  (class class class)co 6842  1st c1st 7364  2nd c2nd 7365  𝑚 cmap 8060  cdom 8158  AC wacn 9015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-map 8062  df-dom 8162  df-acn 9019
This theorem is referenced by:  iundomg  9616  iundom  9617
  Copyright terms: Public domain W3C validator